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  2393  abbi  2406  cleqf  2456  vtoclb  2854  vtoclbg  2857  ceqsexg  2912  elabgf  2925  reu6  2967  ru  3003  sbcbig  3050  sbcnestgf  3141  unineq  3432  preq12bg  3807  axrep1  4148  axrep4  4151  nalset  4167  opthg  4262  opelopabsb  4291  isso2i  4362  orduninsuc  4650  opeliunxp2  4840  resieq  4981  elimasng  5055  cbviota  5240  iota2df  5259  fnbrfvb  5579  fvelimab  5594  fmptco  5707  fsng  5713  fressnfv  5723  isorel  5839  isocnv  5843  isocnv3  5845  isotr  5849  ovg  6002  caovcang  6037  caovordg  6043  caovord3d  6046  caovord  6047  brtpos  6259  dftpos4  6269  fvopab5  6305  omopth  6672  ecopovsym  6776  xpf1o  7039  nneneq  7060  r1pwOLD  7534  karden  7581  infxpenlem  7657  aceq0  7761  cflim2  7905  zfac  8102  ttukeylem1  8152  axextnd  8229  axrepndlem1  8230  axrepndlem2  8231  axrepnd  8232  axacndlem5  8249  zfcndrep  8252  zfcndac  8257  winalim  8333  gruina  8456  ltrnq  8619  ltsosr  8732  ltasr  8738  axpre-lttri  8803  axpre-ltadd  8805  nn0sub  10030  zextle  10101  zextlt  10102  xlesubadd  10599  sqeqor  11233  nn0opth2  11303  rexfiuz  11847  climshft  12066  rpnnen2lem10  12518  dvdsext  12595  sadcadd  12665  dvdssq  12755  isprm2lem  12781  rpexp  12815  pcdvdsb  12937  imasleval  13459  isacs2  13571  acsfiel  13572  funcres2b  13787  pospropd  14254  isnsg  14662  nsgbi  14664  elnmz  14672  nmzbi  14673  oddvdsnn0  14875  odeq  14881  odmulg  14885  isslw  14935  slwispgp  14938  gsumval3  15207  gsumcom2  15242  abveq0  15607  cnt0  17090  kqfvima  17437  kqt0lem  17443  isr0  17444  r0cld  17445  regr1lem2  17447  nrmr0reg  17456  isfildlem  17568  xmeteq0  17919  imasf1oxmet  17955  comet  18075  dscmet  18111  nrmmetd  18113  tngngp  18186  mbfsup  19035  mbfinf  19036  degltlem1  19474  logltb  19969  cxple2  20060  rlimcnp  20276  rlimcnp2  20277  isppw2  20369  sqf11  20393  nmlno0i  21388  nmlno0  21389  blocn  21401  ubth  21468  hvsubeq0  21663  hvaddcan  21665  hvsubadd  21672  normsub0  21731  hlim2  21787  pjoc1  22029  pjoc2  22034  chne0  22089  chsscon3  22095  chlejb1  22107  chnle  22109  h1de2ci  22151  elspansn  22161  elspansn2  22162  cmbr3  22203  cmcm  22209  cmcm3  22210  pjch1  22265  pjch  22289  pj11  22309  pjnel  22321  eigorth  22434  elnlfn  22524  nmlnop0  22594  lnopeq  22605  lnopcon  22631  lnfncon  22652  pjdifnormi  22763  chrelat2  22966  cvexch  22970  mdsym  23008  fmptcof2  23244  cvmlift2lem12  23860  cvmlift2lem13  23861  eupath2lem3  23918  abs2sqle  24031  abs2sqlt  24032  dfpo2  24183  axextdist  24227  brimageg  24537  brdomaing  24545  brrangeg  24546  funpartlem  24552  elhf2  24877  onsuct0  24952  wl-pm5.74  24990  wl-pm5.32  24991  tpssg  25035  alexeqd  25065  snelpwg  25194  oriso  25317  cmppfd  25848  ishomd  25893  sgplpte21b  26237  nn0prpwlem  26341  nn0prpw  26342  prdsbnd2  26622  isdrngo1  26690  zindbi  27134  divalgmodcl  27183  wepwsolem  27241  aomclem8  27262  2sbc6g  27718  2sbc5g  27719  lsatcmp  29815  llnexchb2  30680  lautset  30893  lautle  30895
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