Theorem bibi12d 632

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

Hypotheses

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

Assertion

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

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	bibi1d 622	. 2 ⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ θ)))
3		bi12d.2	. . 3 ⊢ (φ → (θ ↔ τ))
4	3	bibi2d 621	. 2 ⊢ (φ → ((χ ↔ θ) ↔ (χ ↔ τ)))
5	2, 4	bitrd 531	1 ⊢ (φ → ((ψ ↔ θ) ↔ (χ ↔ τ)))

Syntax hints:   → wi 3   ↔ wb 146

This theorem is referenced by:  bi2bian9 637  cleqf 1567  vtoclb 1852  vtoclbg 1855  ceqsexg 1894  elabgf 1905  reu3 1938  ru 1945  sbcbidig 1983  sbceqdig 2023  unineq 2266  elpwg 2417  prssg 2486  elintg 2555  axrep4 2712  nalset 2727  opthgg 2805  so 2880  reuuni2f 2899  orduninsuc 3130  opelcog 3306  resieq 3392  elimasng 3443  eliniseg 3445  asymref2 3456  cnvopab 3461  fnbrfvb 3769  funbrfvbg 3773  eqfnfv 3813  fressnfv 3854  isorel 3910  isocnv 3912  isotr 3913  isotrALT 3914  caoprord 4072  erth 4298  ecopoprsym 4328  pw2en 4465  nneneq 4532  rankr1g 4692  r1pw 4703  karden 4743  aceq0 4747  axac 4762  axextnd 4963  axrepndlem1 4964  axrepndlem2 4965  axrepnd 4966  axacndlem5 4983  zfcndrep 4986  zfcndac 4991  ltpiord 5035  ltsopq 5095  ltapq 5096  ltmpq 5097  ltsosr 5223  ltasr 5229  ltsor 5281  pre-axltadd 5309  addcan 5372  subaddi 5391  subadd 5395  neg11 5429  ltadd1 5643  leadd1 5645  ltsubadd 5647  lesubadd 5649  ltneg 5675  leneg 5677  lesub0 5698  mulcant2i 5708  mulcant2iOLD 5709  mul0or 5716  divmuli 5725  divmulzi 5726  divmul 5727  divmulOLD 5728  div11 5776  rec11i 5790  redivcli 5810  eqneg 5817  ltmul1 5842  ltdiv1 5861  ltdiv1OLD 5862  ltmuldiv 5875  ltmuldivOLD 5876  ltreci 5893  ltrec 5898  lerec 5899  lt2msq 5900  le2msq 5917  nnsub 5971  halfpos 6050  nn0sub 6193  zltp1le 6213  zextle 6224  zextlt 6225  nneo 6233  sq11 6660  sqeqor 6680  discrlem2 6689  nn0opth2 6700  sqrlem12 6716  sqrle 6745  sqr00 6746  sqr2irrlem5 6760  cru 6770  replim 6793  cjreb 6832  abs00 6885  abslt 6912  absle 6913  absgt0 6925  climfnn 7124  iserzshft2i 7139  reef11 7441  reefiso 7460  meteq0 7838  cnid 8152  mulid 8157  nmlno0i 8479  nmlno0 8480  blocn 8492  cosh111 8741  logltb 8800  hvsubeq0 8959  hvaddcan 8961  hvsubadd 8968  normsub0 9027  hilid 9052  projlem1 9210  pjthlem9 9251  pjoc1 9291  pjoc2 9296  shlub 9378  chne0 9441  chsscon3 9447  chlejb1 9459  chnle 9461  h1de2cti 9503  elspansn 9513  elspansn2 9514  cmbr3 9575  cmcm 9581  cmcm3 9582  pjch1 9639  pjch 9663  pj11 9683  pjnel 9695  eigorth 9788  nmlnop0 9947  lnopeq 9958  lnopcon 9988  lnfncon 10015  pjdifnormti 10119  chrelat2 10322  cvexch 10326  mdsym 10364  abs2sqlet 10399  abs2sqltt 10400  homcard 10572  cmppfd 10699  ishomd 10739

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain