MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi12d Structured version   Unicode version

Theorem bibi12d 313
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
imbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
bibi12d  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  ta ) ) )

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bibi1d 311 . 2  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43bibi2d 310 . 2  |-  ( ph  ->  ( ( ch  <->  th )  <->  ( ch  <->  ta ) ) )
52, 4bitrd 245 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bi2bian9  846  xorbi12d  1324  cleqh  2533  abbi  2546  cleqf  2596  vtoclb  3009  vtoclbg  3012  ceqsexg  3067  elabgf  3080  reu6  3123  ru  3160  sbcbig  3207  sbcnestgf  3298  unineq  3591  preq12bg  3977  axrep1  4321  axrep4  4324  nalset  4340  opthg  4436  opelopabsb  4465  isso2i  4535  orduninsuc  4823  opeliunxp2  5013  resieq  5156  elimasng  5230  cbviota  5423  iota2df  5442  fnbrfvb  5767  fvelimab  5782  fmptco  5901  fsng  5907  fressnfv  5920  isorel  6046  isocnv  6050  isocnv3  6052  isotr  6056  ovg  6212  caovcang  6248  caovordg  6254  caovord3d  6257  caovord  6258  brtpos  6488  dftpos4  6498  fvopab5  6534  omopth  6901  ecopovsym  7006  xpf1o  7269  nneneq  7290  r1pwOLD  7772  karden  7819  infxpenlem  7895  aceq0  7999  cflim2  8143  zfac  8340  ttukeylem1  8389  axextnd  8466  axrepndlem1  8467  axrepndlem2  8468  axrepnd  8469  axacndlem5  8486  zfcndrep  8489  zfcndac  8494  winalim  8570  gruina  8693  ltrnq  8856  ltsosr  8969  ltasr  8975  axpre-lttri  9040  axpre-ltadd  9042  nn0sub  10270  zextle  10343  zextlt  10344  xlesubadd  10842  sqeqor  11495  nn0opth2  11565  rexfiuz  12151  climshft  12370  rpnnen2lem10  12823  dvdsext  12900  sadcadd  12970  dvdssq  13060  isprm2lem  13086  rpexp  13120  pcdvdsb  13242  imasleval  13766  isacs2  13878  acsfiel  13879  funcres2b  14094  pospropd  14561  isnsg  14969  nsgbi  14971  elnmz  14979  nmzbi  14980  oddvdsnn0  15182  odeq  15188  odmulg  15192  isslw  15242  slwispgp  15245  gsumval3  15514  gsumcom2  15549  abveq0  15914  cnt0  17410  kqfvima  17762  kqt0lem  17768  isr0  17769  r0cld  17770  regr1lem2  17772  nrmr0reg  17781  isfildlem  17889  cnextfvval  18096  xmeteq0  18368  imasf1oxmet  18405  comet  18543  dscmet  18620  nrmmetd  18622  tngngp  18695  mbfsup  19556  mbfinf  19557  degltlem1  19995  logltb  20494  cxple2  20588  rlimcnp  20804  rlimcnp2  20805  isppw2  20898  sqf11  20922  eupath2lem3  21701  nmlno0i  22295  nmlno0  22296  blocn  22308  ubth  22375  hvsubeq0  22570  hvaddcan  22572  hvsubadd  22579  normsub0  22638  hlim2  22694  pjoc1  22936  pjoc2  22941  chne0  22996  chsscon3  23002  chlejb1  23014  chnle  23016  h1de2ci  23058  elspansn  23068  elspansn2  23069  cmbr3  23110  cmcm  23116  cmcm3  23117  pjch1  23172  pjch  23196  pj11  23216  pjnel  23228  eigorth  23341  elnlfn  23431  nmlnop0  23501  lnopeq  23512  lnopcon  23538  lnfncon  23559  pjdifnormi  23670  chrelat2  23873  cvexch  23877  mdsym  23915  fmptcof2  24076  cvmlift2lem12  25001  cvmlift2lem13  25002  abs2sqle  25120  abs2sqlt  25121  dfpo2  25378  axextdist  25427  brimageg  25772  brdomaing  25780  brrangeg  25781  elhf2  26116  onsuct0  26191  wl-pm5.74  26228  wl-pm5.32  26229  nn0prpwlem  26325  nn0prpw  26326  prdsbnd2  26504  isdrngo1  26572  zindbi  27009  divalgmodcl  27058  wepwsolem  27116  aomclem8  27136  2sbc6g  27592  2sbc5g  27593  lsatcmp  29801  llnexchb2  30666  lautset  30879  lautle  30881
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator