Theorem bibi12d 629

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

Hypotheses

Ref	Expression
bi12d.1	|- (ph -> (ps <-> ch))
bi12d.2	|- (ph -> (th <-> ta))

Assertion

Ref	Expression
bibi12d	|- (ph -> ((ps <-> th) <-> (ch <-> ta)))

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	bibi1d 619	. 2 |- (ph -> ((ps <-> th) <-> (ch <-> th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	bibi2d 618	. 2 |- (ph -> ((ch <-> th) <-> (ch <-> ta)))
5	2, 4	bitrd 528	1 |- (ph -> ((ps <-> th) <-> (ch <-> ta)))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  bi2bian9 634  cleqf 1560  vtoclb 1845  vtoclbg 1848  ceqsexg 1887  elabgf 1898  reu3 1931  ru 1938  sbcbidig 1973  sbceqdig 2012  unineq 2255  elpwg 2405  prssg 2472  elintg 2541  axrep4 2697  nalset 2712  opthgg 2789  so 2864  reuuni2f 2883  orduninsuc 3114  opelcog 3290  resieq 3376  elimasng 3427  eliniseg 3429  asymref2 3440  cnvopab 3445  fnbrfvb 3753  funbrfvbg 3757  eqfnfv 3797  fressnfv 3838  isorel 3894  isocnv 3896  isotr 3897  isotrALT 3898  caoprord 4056  erth 4282  ecopoprsym 4310  pw2en 4446  nneneq 4512  rankr1g 4675  r1pw 4686  karden 4726  aceq0 4730  axac 4745  axextnd 4943  axrepndlem1 4944  axrepndlem2 4945  axrepnd 4946  axacndlem5 4963  zfcndrep 4966  zfcndac 4971  ltpiord 5015  ltsopq 5075  ltapq 5076  ltmpq 5077  ltsosr 5203  ltasr 5209  ltsor 5261  pre-axltadd 5289  addcant 5352  subadd 5371  subaddt 5375  neg11t 5409  ltadd1t 5623  leadd1t 5625  ltsubaddt 5627  lesubaddt 5629  ltnegt 5655  lenegt 5657  lesub0t 5678  mulcant2 5688  mulcant2OLD 5689  mul0ort 5696  divmul 5705  divmulz 5706  divmult 5707  div11t 5765  rec11 5778  redivcl 5798  eqnegt 5805  ltmul1t 5830  ltdiv1t 5849  ltdiv1tOLD 5850  ltmuldivt 5863  ltmuldivtOLD 5864  ltrec 5879  ltrect 5884  lerect 5885  lt2msqt 5886  le2msqt 5903  nnsubt 5957  halfpost 6036  nn0subt 6161  zltp1let 6181  zextlet 6189  zextltt 6190  nneot 6198  sq11t 6629  sqeqort 6649  discrlem2 6657  nn0opth2t 6668  sqrlem12 6684  sqrlet 6713  sqr00t 6714  sqr2irrlem5 6728  crut 6738  replimt 6761  cjrebt 6800  abs00t 6853  absltt 6880  abslet 6881  absgt0t 6893  climfnn 7092  iserzshft2 7107  reef11t 7409  reefiso 7428  meteq0 7812  cnid 8127  mulid 8132  nmlno0i 8454  nmlno0 8455  blocn 8467  cosh111t 8717  logltbt 8776  hvsubeq0t 8935  hvaddcant 8937  hvsubaddt 8944  normsub0t 9003  hilid 9028  projlem1 9186  pjthlem9 9227  pjoc1t 9267  pjoc2t 9272  shlubt 9354  chne0t 9417  chsscon3t 9423  chlejb1t 9435  chnlet 9437  h1de2ct 9479  elspansnt 9489  elspansn2t 9490  cmbr3t 9551  cmcmt 9557  cmcm3t 9558  pjch1t 9615  pjcht 9639  pj11t 9659  pjnelt 9671  eigortht 9764  nmlnop0t 9923  lnopeqt 9934  lnopcont 9964  lnfncont 9991  pjdifnormt 10095  chrelat2t 10297  cvexcht 10301  mdsymt 10339  abs2sqlet 10374  abs2sqltt 10375  homcard 10539  cmppfd 10678  ishomd 10718

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