Theorem bibi12d 691

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

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

This theorem is referenced by:  bi2bian9 696  cleqf 1984  vtoclb 2344  vtoclbg 2347  ceqsexg 2392  elabgf 2404  reu6 2443  ru 2451  sbcbidig 2499  sbceqdigOLD 2555  unineq 2844  elpwg 3038  prssgOLD 3141  elintg 3222  axrep4 3432  nalset 3448  opthgg 3534  so 3620  reuuni1 3808  reuuni2f 3810  orduninsuc 3925  opelco2g 4133  resieq 4227  elimasng 4291  elinisegOLD 4295  asymref2OLD 4311  cnvopabOLD 4318  fnbrfvb 4712  funbrfvbg 4716  fvelimab 4725  eqfnfv 4766  fressnfv 4813  isorel 4871  isocnv 4873  isotr 4874  isotrALT 4875  caoprord 4989  reiota2f 5109  erth 5340  ecopoprsym 5369  pw2en 5505  nneneq 5606  rankr1g 5786  r1pw 5797  karden 5856  aceq0 5892  zfac 5907  axextnd 6095  axrepndlem1 6096  axrepndlem2 6097  axrepnd 6098  axacndlem5 6115  zfcndrep 6118  zfcndac 6123  ltpiord 6167  ltsopq 6227  ltapq 6228  ltmpq 6229  ltsosr 6355  ltasr 6361  ltsor 6413  pre-axltadd 6442  addcan 6507  subadd 6532  neg11 6569  ltadd1 6806  leadd1 6808  ltsubadd 6810  lesubadd 6812  ltneg 6844  leneg 6846  lesub0 6867  mulcant2i 6879  mul0or 6884  divmulzi 6895  divmul 6896  div11 6941  rec11i 6954  redivcli 6976  eqneg 6983  ltmul1 7008  ltdiv1 7031  ltdiv1OLD 7032  ltmuldiv 7045  ltmuldivOLD 7046  ltreci 7062  ltrec 7067  lerec 7068  lt2msq 7069  le2msq 7086  nnsub 7141  halfpos 7222  nn0sub 7370  zltp1le 7390  zextle 7401  zextlt 7402  nneo 7410  sq11 7874  sqeqor 7895  discrlem2 7907  nn0opth2 7918  sqrlem12 7934  sqrle 7963  sqr00 7964  sqr2irrlem5 7978  cru 7988  replim 8011  cjreb 8050  abs00 8104  abslt 8132  absle 8133  absgt0 8145  climfnn 8352  iserzshft2i 8367  reef11 8674  reefiso 8693  meteq0 9089  cnid 9435  mulid 9440  nmlno0i 9794  nmlno0 9795  blocn 9807  cosh111 10071  logltb 10130  issubsplem1 10246  issubspt 10247  on1el3 10412  hvsubeq0 10567  hvaddcan 10569  hvsubadd 10577  normsub0 10636  hilid 10661  projlem1 10819  pjthlem9 10860  pjoc1 10900  pjoc2 10905  shlub 10987  chne0 11050  chsscon3 11056  chlejb1 11068  chnle 11070  h1de2ci 11112  elspansn 11122  elspansn2 11123  cmbr3 11184  cmcm 11190  cmcm3 11191  pjch1 11250  pjch 11274  pj11 11294  pjnel 11306  eigorth 11401  nmlnop0 11560  lnopeq 11571  lnopcon 11601  lnfncon 11628  pjdifnormi 11739  chrelat2 11942  cvexch 11946  mdsym 11984  bnj90OLD 12446  bnj147 12480  bnj148 12481  bnj209OLD 12501  bnj210OLD 12503  bnj211OLD 12505  bnj1306 13049  bnj1310 13050  bnj1492 13161  bnj609 13306  fz1eqb 13609  abs2sqle 13624  abs2sqlt 13625  isprm2lem 13774  epelg 13827  ordsucuniel 13863  axextdist 13866  brsset 14069  brbigcup 14074  elfix2 14078  fatesg 14293  elintabg 14414  snelpwg 14415  surjsec2 14467  homcard 14893  cmppfd 15092  ishomd 15139  tarvalg 15213  cbvsbcOLD 15355  inficlALT 15372  cnconn 15444  neibastop3 15524  oprabvalg 15706  erthdmg 15730  add20 15777  iserzshft2 15829  txmet 15925  isdivrng1 16109  2sbc6g 16379  2sbc5g 16380  cbviotaf 16432

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 164  df-an 242

Copyright terms: Public domain