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

Theorem bibi12d 312
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 310 . 2  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43bibi2d 309 . 2  |-  ( ph  ->  ( ( ch  <->  th )  <->  ( ch  <->  ta ) ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bi2bian9  845  xorbi12d  1306  cleqh  2380  abbi  2393  cleqf  2443  vtoclb  2841  vtoclbg  2844  ceqsexg  2899  elabgf  2912  reu6  2954  ru  2990  sbcbig  3037  sbcnestgf  3128  unineq  3419  preq12bg  3791  axrep1  4132  axrep4  4135  nalset  4151  opthg  4246  opelopabsb  4275  isso2i  4346  orduninsuc  4634  opeliunxp2  4824  resieq  4965  elimasng  5039  cbviota  5224  iota2df  5243  fnbrfvb  5563  fvelimab  5578  fmptco  5691  fsng  5697  fressnfv  5707  isorel  5823  isocnv  5827  isocnv3  5829  isotr  5833  ovg  5986  caovcang  6021  caovordg  6027  caovord3d  6030  caovord  6031  brtpos  6243  dftpos4  6253  fvopab5  6289  omopth  6656  ecopovsym  6760  xpf1o  7023  nneneq  7044  r1pwOLD  7518  karden  7565  infxpenlem  7641  aceq0  7745  cflim2  7889  zfac  8086  ttukeylem1  8136  axextnd  8213  axrepndlem1  8214  axrepndlem2  8215  axrepnd  8216  axacndlem5  8233  zfcndrep  8236  zfcndac  8241  winalim  8317  gruina  8440  ltrnq  8603  ltsosr  8716  ltasr  8722  axpre-lttri  8787  axpre-ltadd  8789  nn0sub  10014  zextle  10085  zextlt  10086  xlesubadd  10583  sqeqor  11217  nn0opth2  11287  rexfiuz  11831  climshft  12050  rpnnen2lem10  12502  dvdsext  12579  sadcadd  12649  dvdssq  12739  isprm2lem  12765  rpexp  12799  pcdvdsb  12921  imasleval  13443  isacs2  13555  acsfiel  13556  funcres2b  13771  pospropd  14238  isnsg  14646  nsgbi  14648  elnmz  14656  nmzbi  14657  oddvdsnn0  14859  odeq  14865  odmulg  14869  isslw  14919  slwispgp  14922  gsumval3  15191  gsumcom2  15226  abveq0  15591  cnt0  17074  kqfvima  17421  kqt0lem  17427  isr0  17428  r0cld  17429  regr1lem2  17431  nrmr0reg  17440  isfildlem  17552  xmeteq0  17903  imasf1oxmet  17939  comet  18059  dscmet  18095  nrmmetd  18097  tngngp  18170  mbfsup  19019  mbfinf  19020  degltlem1  19458  logltb  19953  cxple2  20044  rlimcnp  20260  rlimcnp2  20261  isppw2  20353  sqf11  20377  nmlno0i  21372  nmlno0  21373  blocn  21385  ubth  21452  hvsubeq0  21647  hvaddcan  21649  hvsubadd  21656  normsub0  21715  hlim2  21771  pjoc1  22013  pjoc2  22018  chne0  22073  chsscon3  22079  chlejb1  22091  chnle  22093  h1de2ci  22135  elspansn  22145  elspansn2  22146  cmbr3  22187  cmcm  22193  cmcm3  22194  pjch1  22249  pjch  22273  pj11  22293  pjnel  22305  eigorth  22418  elnlfn  22508  nmlnop0  22578  lnopeq  22589  lnopcon  22615  lnfncon  22636  pjdifnormi  22747  chrelat2  22950  cvexch  22954  mdsym  22992  fmptcof2  23229  cvmlift2lem12  23845  cvmlift2lem13  23846  eupath2lem3  23903  abs2sqle  24016  abs2sqlt  24017  dfpo2  24112  axextdist  24156  brimageg  24466  brdomaing  24474  brrangeg  24475  elhf2  24805  onsuct0  24880  wl-pm5.74  24918  wl-pm5.32  24919  tpssg  24932  alexeqd  24962  snelpwg  25091  oriso  25214  cmppfd  25745  ishomd  25790  sgplpte21b  26134  nn0prpwlem  26238  nn0prpw  26239  prdsbnd2  26519  isdrngo1  26587  zindbi  27031  divalgmodcl  27080  wepwsolem  27138  aomclem8  27159  2sbc6g  27615  2sbc5g  27616  lsatcmp  29193  llnexchb2  30058  lautset  30271  lautle  30273
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 177
  Copyright terms: Public domain W3C validator