Theorem bibi12d 628

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 618	. 2 |- (ph -> ((ps <-> th) <-> (ch <-> th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	bibi2d 617	. 2 |- (ph -> ((ch <-> th) <-> (ch <-> ta)))
5	2, 4	bitrd 527	1 |- (ph -> ((ps <-> th) <-> (ch <-> ta)))

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

This theorem is referenced by:  bi2bian9 633  cleqf 1557  vtoclb 1841  vtoclbg 1844  ceqsexg 1883  elabgf 1894  reu3 1927  ru 1934  sbcbidig 1969  sbceqdig 2008  unineq 2251  elpwg 2401  prssg 2468  elintg 2536  axrep4 2692  nalset 2707  opthgg 2784  so 2859  reuuni2f 2878  orduninsuc 3109  opelcog 3285  resieq 3368  elimasng 3419  eliniseg 3421  asymref2 3432  cnvopab 3437  fnbrfvb 3744  funbrfvbg 3748  eqfnfv 3788  fressnfv 3829  isorel 3885  isocnv 3887  isotr 3888  isotrALT 3889  caoprord 4048  erth 4272  ecopoprsym 4300  pw2en 4432  nneneq 4498  rankr1g 4655  r1pw 4666  karden 4706  aceq0 4710  axac 4725  axextnd 4923  axrepndlem1 4924  axrepndlem2 4925  axrepnd 4926  axacndlem5 4943  zfcndrep 4946  zfcndac 4951  ltpiord 4995  ltsopq 5055  ltapq 5056  ltmpq 5057  ltsosr 5183  ltasr 5189  ltsor 5241  pre-axltadd 5269  addcant 5332  subadd 5351  subaddt 5355  neg11t 5389  ltadd1t 5605  leadd1t 5607  ltsubaddt 5609  lesubaddt 5611  ltnegt 5636  lenegt 5638  lesub0t 5659  mulcant2 5668  mul0ort 5673  divmul 5682  divmulz 5683  divmult 5684  div11t 5729  rec11 5742  redivcl 5762  eqnegt 5769  ltmul1t 5794  ltdiv1t 5813  ltmuldivt 5825  ltrec 5835  ltrect 5840  lerect 5841  lt2msqt 5842  le2msqt 5859  nnsubt 5912  halfpost 5991  nn0subt 6116  zltp1let 6136  zextlet 6144  zextltt 6145  nneot 6153  sq0t 6558  sq11t 6568  sqeqort 6588  discrlem2 6595  nn0opth2t 6606  sqrlem12 6622  sqrlet 6651  sqr00t 6652  sqr2irrlem5 6666  crut 6676  replimt 6700  cjrebt 6743  abs00t 6796  absltt 6825  abslttOLD 6826  abslet 6827  absgt0t 6839  climfnn 7038  iserzshft2 7052  reeff1 7358  reefiso 7378  meteq0 7762  cnid 8079  mulid 8084  nmlno0i 8399  nmlno0 8400  blocn 8411  cosh111t 8651  logltbt 8715  hvsubeq0t 8874  hvaddcant 8876  hvsubaddt 8883  normsub0t 8942  hilid 8967  projlem1 9125  pjthlem9 9165  pjoc1t 9205  pjoc2t 9210  shlubt 9292  chne0t 9355  chsscon3t 9361  chlejb1t 9373  chnlet 9375  h1de2ct 9418  elspansnt 9428  elspansn2t 9429  cmbr3t 9491  cmcmt 9497  cmcm3t 9498  pjch1t 9555  pjcht 9579  pj11t 9599  pjnelt 9611  eigortht 9704  nmlnop0t 9861  lnopeqt 9872  lnopcont 9902  lnfncont 9929  pjdifnormt 10033  chrelat2t 10234  cvexcht 10238  mdsymt 10276  abs2sqlet 10308  abs2sqltt 10309  homcard 10462  cmppfd 10558  ishomd 10598

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