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

Theorem 3bitr4d 276
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
Hypotheses
Ref Expression
3bitr4d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr4d.2  |-  ( ph  ->  ( th  <->  ps )
)
3bitr4d.3  |-  ( ph  ->  ( ta  <->  ch )
)
Assertion
Ref Expression
3bitr4d  |-  ( ph  ->  ( th  <->  ta )
)

Proof of Theorem 3bitr4d
StepHypRef Expression
1 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
2 3bitr4d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
3 3bitr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
42, 3bitr4d 247 . 2  |-  ( ph  ->  ( ps  <->  ta )
)
51, 4bitrd 244 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sbcom  2042  sbcom2  2066  r19.12sn  3709  ordsucelsuc  4629  ordsucsssuc  4630  fvopab3g  5614  fvimacnvALT  5660  respreima  5670  fmptco  5707  fnsuppres  5748  cocan1  5817  cocan2  5818  smoword  6399  oaword  6563  omword  6584  om00el  6590  oeword  6604  nnaword  6641  nnmword  6647  swoer  6704  erth  6720  brecop  6767  eceqoveq  6779  xpdom2  6973  pw2f1olem  6982  omsucdomOLD  7072  fisucdomOLD  7082  ixpfi2  7170  cantnfrescl  7394  rankr1bg  7491  r1pwcl  7535  fseqenlem1  7667  alephord3  7721  alephdom2  7730  engch  8266  fpwwe2lem7  8274  fpwwe2lem9  8276  ltexpi  8542  ltapi  8543  ltmpi  8544  ltsonq  8609  ltmnq  8612  1idpr  8669  addcanpr  8686  axpre-ltadd  8805  axlttri  8910  subsub23  9072  leadd1  9258  ltsub1  9286  ltsub2  9287  leord1  9316  eqord1  9317  lemul1  9624  lediv1  9637  lt2mul2div  9648  lerec  9654  lediv2  9662  le2msq  9672  suprleub  9734  infmrgelb  9750  ofsubeq0  9759  ofsubge0  9761  avgle1  9967  avgle2  9968  cnref1o  10365  xleneg  10561  xltadd1  10592  xsubge0  10597  xposdif  10598  xltmul1  10628  supxrleub  10661  infmxrgelb  10669  iooneg  10772  iccneg  10773  iccsplit  10784  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  fzsplit2  10831  fzaddel  10842  fzrev  10862  elfzo  10893  elfzom1b  10934  negmod0  10995  leexp2  11172  ltexp2r  11174  cjreb  11624  sqrlt  11763  rexfiuz  11847  limsuplt  11969  o1lo1  12027  rlimresb  12055  lo1eq  12058  rlimeq  12059  o1eq  12060  isercoll  12157  efle  12414  tanaddlem  12462  nndivdvds  12553  moddvds  12554  oddm1even  12604  bitsp1  12638  sadcaddlem  12664  sadadd  12674  sadass  12678  bitsshft  12682  smuval2  12689  smumul  12700  dvdssq  12755  phiprmpw  12860  eulerthlem2  12866  odzdvds  12876  pc2dvds  12947  1arith  12990  imasleval  13459  mreacs  13576  catpropd  13628  oppcsect  13692  funcres2b  13787  fthsect  13815  fthinv  13816  fucsect  13862  fucinv  13863  latnlemlt  14206  latnle  14207  ipole  14277  ipolt  14278  spwex  14354  issubg3  14653  eqgid  14685  resghm2b  14717  conjghm  14729  gastacos  14780  resscntz  14823  cntzrec  14825  oppgsubm  14851  oppgsubg  14852  sylow3lem6  14959  lsmcom2  14982  lsmass  14995  lsmcomx  15164  subgdmdprd  15285  opprsubrg  15582  lsslss  15734  lbspropd  15868  islbs2  15923  rspsn  16022  psrbagconf1o  16136  gsumbagdiaglem  16137  mplmonmul  16224  prmirred  16464  znfld  16530  basdif0  16707  restlp  16929  cnrest2  17030  cnprest  17033  cnprest2  17034  lmss  17042  lmff  17045  ist1-2  17091  lpcls  17108  perfcls  17109  cmpfi  17151  hauseqlcld  17356  txlm  17358  txkgen  17362  xkopt  17365  idqtop  17413  tgqtop  17419  qtopcn  17421  uffix  17632  fmco  17672  flimrest  17694  lmflf  17716  txflf  17717  fclsrest  17735  cnpfcf  17752  tsmsgsum  17837  tsmsres  17842  tsmsf1o  17843  ismet2  17914  imasf1oxmet  17955  blres  17993  xmetec  17996  imasf1obl  18050  imasf1oxms  18051  prdsbl  18053  stdbdbl  18079  metrest  18086  tngngp  18186  cnbl0  18299  cnblcld  18300  bl2ioo  18314  cncfcnvcn  18440  iihalf2  18447  icoopnst  18453  iocopnst  18454  icopnfcnv  18456  icopnfhmeo  18457  cphorthcom  18652  caucfil  18725  lmclim  18744  cmsss  18788  volsup  18929  dyaddisjlem  18966  mbfeqalem  19013  mbfeqa  19014  mbfmulc2lem  19018  mbfmax  19020  mbfposr  19023  ismbf3d  19025  mbfimaopnlem  19026  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  0plef  19043  0pledm  19044  i1fmulclem  19073  i1fres  19076  i1fpos  19077  itg1climres  19085  mbfi1fseqlem4  19089  itg2mulclem  19117  itg2monolem1  19121  itg2cnlem1  19132  iblre  19164  iblcn  19169  itgeqa  19184  ellimc2  19243  limcflf  19247  dvreslem  19275  lhop1  19377  ply1remlem  19564  fta1glem2  19568  ofmulrt  19678  plydiveu  19694  plyremlem  19700  quotcan  19705  ulmres  19783  cos11  19911  logleb  19973  argrege0  19981  logdivle  19989  efopn  20021  logccv  20026  cxplt  20057  cxple  20058  cxple2  20060  cxplt2  20061  cxplt3  20063  cxple3  20064  angrtmuld  20122  quad2  20151  atans2  20243  rlimcnp  20276  rlimcnp2  20277  rlimcxp  20284  sqff1o  20436  fsumvma2  20469  dchrptlem2  20520  lgsdilem  20577  lgsne0  20588  lgsqr  20601  lgsquadlem1  20609  lgsquadlem2  20610  m1lgs  20617  dchrisum0lem1  20681  padicabv  20795  rngosn3  21109  nvsubsub23  21236  nmorepnf  21362  blocnilem  21398  ubthlem1  21465  shscom  21914  pjpreeq  21993  spansncol  22163  cmcm2  22211  hodsi  22371  nmoprepnf  22463  nmfnrepnf  22476  pjssposi  22768  cvcon3  22880  mdsymlem8  23006  dmdsym  23009  unipreima  23224  fmptcof2  23244  xrge0iifiso  23332  logblt  23423  indpi1  23620  indf1ofs  23624  subfacp1lem3  23728  subfacp1lem5  23730  eupath2lem3  23918  predfz  24274  elfuns  24525  colinearalglem2  24607  axcgrid  24616  cgrcomr  24692  ofscom  24702  cgr3permute3  24742  cgr3permute1  24743  cgr3com  24748  colinearperm1  24757  colinearperm3  24758  outsideofcom  24823  itg2addnclem2  25004  areacirclem6  25033  areacirc  25034  dupre1  25346  prsubrtr  25502  vtarsuelt  25998  pdiveql  26271  opnbnd  26346  filnetlem4  26433  caures  26579  cnpwstotbnd  26624  ismtyima  26630  rrnmet  26656  reheibor  26666  fnnfpeq0  26861  lzenom  26952  rmxycomplete  27105  fzneg  27172  modabsdifz  27181  jm2.19  27189  pw2f1ocnv  27233  lindfmm  27400  lindsmm  27401  lsslindf  27403  lsslinds  27404  islindf4  27411  caofcan  27643  rfcnpre1  27793  rfcnpre2  27805  fzon  28212  usgraeq12d  28245  nbgrasym  28286  sbcomwAUX7  29562  sbcomOLD7  29709  sbcom2OLD7  29715  lcvbr  29833  lkrsc  29909  lshpkrlem1  29922  opltcon3b  30016  cmt2N  30062  cmt3N  30063  cvrcon3b  30089  cvrcmp2  30096  cvlexchb2  30143  cvlatexchb2  30147  2llnmj  30371  4atlem3  30407  4atlem9  30414  4atlem10a  30415  4atlem11a  30418  4atlem12a  30421  4at2  30425  2lplnmj  30433  llnexchb2  30680  lautlt  30902  lautcvr  30903  lautco  30908  ltrnatb  30948  ltrneq2  30959  cdlemefrs29pre00  31206  cdlemefrs29cpre1  31209  cdleme32fva  31248  dibglbN  31978  dochsncom  32194  dochkrsat  32267  lspindp5  32582  mapdh8ab  32589  hdmapip0com  32732
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