Theorem bibi12d 477

Description: Deduction joining two equivalences to form equivalence of biconditionals.

Hypotheses

Ref	Expression
bi2d.1	⊢ (φ → (ψ ↔ χ))
bi2d.2	⊢ (φ → (θ ↔ τ))

Assertion

Ref	Expression
bibi12d	⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ τ)))

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		bi2d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	bibi1d 471	. 2 ⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ θ)))
3		bi2d.2	. . 3 ⊢ (φ → (θ ↔ τ))
4	3	bibi2d 470	. 2 ⊢ (φ → ((χ ↔ θ) ↔ (χ ↔ τ)))
5	2, 4	bitrd 406	1 ⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ τ)))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  bi2bian9 480  axac 1085  cleqf 1167  vtoclb 1381  vtoclbg 1384  ceqsexg 1411  elabgf 1416  ru 1437  sbcbi 1463  zfrep2 1475  nalset 1482  unineq 1680  elpwg 1802  reuuni2 1956  elintg 1973  so 2152  orduninsuc 2365  opelcog 2511  resieq 2581  eliniseg 2618  cnvopab 2632  fnfvbr 2855  cleqfv 2880  fvelrn 2883  fressnfv 2898  isorel 2932  isocnv 2934  isotr 2935  isotrALT 2936  caoprord 3070  erth 3219  ecopoprsym 3246  domeng 3285  pw2en 3348  nneneq 3408  rankr1g 3519  r1pw 3529  karden 3551  aceq0 3553  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axrepnd 3740  axacndlem5 3757  zfcndrep 3760  zfcndac 3765  ltpiord 3809  ltsopq 3869  ltapq 3870  ltmpq 3871  ltsosr 3997  ltasr 4003  ltsor 4055  axltadd 4085  addcant 4122  subadd 4143  subaddt 4145  negcon1t 4167  subeq0t 4169  mulcant 4208  mul0ort 4212  divmul 4218  divmulz 4219  divmult 4220  rec11 4262  redivcl 4274  ltadd1t 4348  leadd1t 4350  ltsubaddt 4353  lesubaddt 4355  posdift 4365  ltnegt 4366  lenegt 4368  lesub0t 4374  ltdivt 4404  ltmuldivt 4406  ltrec 4410  ltdiv23 4413  ltrect 4417  lerect 4418  ltdiv23t 4419  le2sqt 4420  nnsubt 4451  halfpost 4508  nn0subt 4587  zltp1let 4597  sqe11t 4705  lt2sqet 4706  discrlem2 4714  nn0opth2t 4726  sqrlem12 4742  sqr00t 4770  sqr2irrlem5 4781  replimt 4798  cjret 4829  absltt 4857  absgt0t 4863  hvsubeq0t 5040  hvsubaddt 5042  hiidrclt 5053  normsub0t 5085  projlem1 5193  pjthlem9 5233  pjoc1t 5270  pjoc2t 5274  shlubt 5355  chsscon3t 5417  chlejb1t 5429  chnlet 5431  chne0t 5452  h1de2ct 5461  elspansnt 5471  elspansn2t 5472  pjch1t 5560  pjcht 5582  pjdifnormt 5637  pjnelt 5667  chrelat2t 5761  cvexcht 5763

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org