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

Theorem 3bitr4d 277
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 248 . 2  |-  ( ph  ->  ( ps  <->  ta )
)
51, 4bitrd 245 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  sbcom  2146  sbcom2  2171  r19.12sn  3840  ordsucelsuc  4769  ordsucsssuc  4770  fvopab3g  5769  fvimacnvALT  5816  respreima  5826  fmptco  5868  fnsuppres  5919  cocan1  5991  cocan2  5992  smoword  6595  oaword  6759  omword  6780  om00el  6786  oeword  6800  nnaword  6837  nnmword  6843  swoer  6900  erth  6916  brecop  6964  eceqoveq  6976  xpdom2  7170  pw2f1olem  7179  omsucdomOLD  7269  fisucdomOLD  7279  ixpfi2  7371  cantnfrescl  7596  rankr1bg  7693  r1pwcl  7737  fseqenlem1  7869  alephord3  7923  alephdom2  7932  engch  8467  fpwwe2lem7  8475  fpwwe2lem9  8477  ltexpi  8743  ltapi  8744  ltmpi  8745  ltsonq  8810  ltmnq  8813  1idpr  8870  addcanpr  8887  axpre-ltadd  9006  axlttri  9111  subsub23  9274  leadd1  9460  ltsub1  9488  ltsub2  9489  leord1  9518  eqord1  9519  lemul1  9826  lediv1  9839  lt2mul2div  9850  lerec  9856  lediv2  9864  le2msq  9874  suprleub  9936  infmrgelb  9952  ofsubeq0  9961  ofsubge0  9963  avgle1  10171  avgle2  10172  cnref1o  10571  xleneg  10768  xltadd1  10799  xsubge0  10804  xposdif  10805  xltmul1  10835  supxrleub  10869  infmxrgelb  10877  iooneg  10981  iccneg  10982  iccsplit  10993  iccshftr  10994  iccshftl  10996  iccdil  10998  icccntr  11000  fzsplit2  11040  fzaddel  11051  fzrev  11072  elfzo  11105  fzon  11121  elfzom1b  11154  negmod0  11219  leexp2  11397  ltexp2r  11399  cjreb  11891  sqrlt  12030  rexfiuz  12114  limsuplt  12236  o1lo1  12294  rlimresb  12322  lo1eq  12325  rlimeq  12326  o1eq  12327  isercoll  12424  efle  12682  tanaddlem  12730  nndivdvds  12821  moddvds  12822  oddm1even  12872  bitsp1  12906  sadcaddlem  12932  sadadd  12942  sadass  12946  bitsshft  12950  smuval2  12957  smumul  12968  dvdssq  13023  phiprmpw  13128  eulerthlem2  13134  odzdvds  13144  pc2dvds  13215  1arith  13258  imasleval  13729  mreacs  13846  catpropd  13898  oppcsect  13962  funcres2b  14057  fthsect  14085  fthinv  14086  fucsect  14132  fucinv  14133  latnlemlt  14476  latnle  14477  ipole  14547  ipolt  14548  spwex  14624  issubg3  14923  eqgid  14955  resghm2b  14987  conjghm  14999  gastacos  15050  resscntz  15093  cntzrec  15095  oppgsubm  15121  oppgsubg  15122  sylow3lem6  15229  lsmcom2  15252  lsmass  15265  lsmcomx  15434  subgdmdprd  15555  opprsubrg  15852  lsslss  16000  lbspropd  16134  islbs2  16189  rspsn  16288  psrbagconf1o  16402  gsumbagdiaglem  16403  mplmonmul  16490  prmirred  16738  znfld  16804  basdif0  16981  neiptopreu  17160  neitr  17206  restlp  17209  cnrest2  17312  cnprest  17315  cnprest2  17316  lmss  17324  lmff  17327  ist1-2  17373  lpcls  17390  perfcls  17391  cmpfi  17433  hauseqlcld  17639  txlm  17641  txkgen  17645  xkopt  17648  idqtop  17699  tgqtop  17705  qtopcn  17707  uffix  17914  fmco  17954  flimrest  17976  lmflf  17998  txflf  17999  fclsrest  18017  cnpfcf  18034  tsmsgsum  18129  tsmsres  18134  tsmsf1o  18135  fmucndlem  18282  ismet2  18324  imasf1oxmet  18366  blres  18422  xmetec  18425  imasf1obl  18479  imasf1oxms  18480  prdsbl  18482  stdbdbl  18508  metrest  18515  metustsymOLD  18552  metustsym  18553  blval2  18566  metuel2  18570  tngngp  18656  cnbl0  18769  cnblcld  18770  bl2ioo  18784  cncfcnvcn  18912  iihalf2  18919  icoopnst  18925  iocopnst  18926  icopnfcnv  18928  icopnfhmeo  18929  cphorthcom  19124  caucfil  19197  lmclim  19216  cmsss  19264  volsup  19411  dyaddisjlem  19448  mbfeqalem  19495  mbfeqa  19496  mbfmulc2lem  19500  mbfmax  19502  mbfposr  19505  ismbf3d  19507  mbfimaopnlem  19508  mbfaddlem  19513  mbfsup  19517  mbfinf  19518  0plef  19525  0pledm  19526  i1fmulclem  19555  i1fres  19558  i1fpos  19559  itg1climres  19567  mbfi1fseqlem4  19571  itg2mulclem  19599  itg2monolem1  19603  itg2cnlem1  19614  iblre  19646  iblcn  19651  itgeqa  19666  ellimc2  19725  limcflf  19729  dvreslem  19757  lhop1  19859  ply1remlem  20046  fta1glem2  20050  ofmulrt  20160  plydiveu  20176  plyremlem  20182  quotcan  20187  ulmres  20265  cos11  20396  logleb  20459  argrege0  20467  logdivle  20478  efopn  20510  logccv  20515  cxplt  20546  cxple  20547  cxple2  20549  cxplt2  20550  cxplt3  20552  cxple3  20553  angrtmuld  20611  quad2  20640  atans2  20732  rlimcnp  20765  rlimcnp2  20766  rlimcxp  20773  sqff1o  20926  fsumvma2  20959  dchrptlem2  21010  lgsdilem  21067  lgsne0  21078  lgsqr  21091  lgsquadlem1  21099  lgsquadlem2  21100  m1lgs  21107  dchrisum0lem1  21171  padicabv  21285  uhgraeq12d  21303  usgraeq12d  21346  nbgrasym  21410  cusgrauvtxb  21466  eupath2lem3  21662  rngosn3  21975  nvsubsub23  22104  nmorepnf  22230  blocnilem  22266  ubthlem1  22333  shscom  22782  pjpreeq  22861  spansncol  23031  cmcm2  23079  hodsi  23239  nmoprepnf  23331  nmfnrepnf  23344  pjssposi  23636  cvcon3  23748  mdsymlem8  23874  dmdsym  23877  unipreima  24017  fmptcof2  24037  1stpreima  24056  metider  24250  pstmxmet  24253  xrge0iifiso  24282  logblt  24367  indpi1  24380  indf1ofs  24384  aean  24556  brfae  24560  subfacp1lem3  24829  subfacp1lem5  24831  predfz  25425  elfuns  25676  colinearalglem2  25758  axcgrid  25767  cgrcomr  25843  ofscom  25853  cgr3permute3  25893  cgr3permute1  25894  cgr3com  25899  colinearperm1  25908  colinearperm3  25909  outsideofcom  25974  itg2addnclem2  26164  areacirclem6  26194  areacirc  26195  opnbnd  26226  filnetlem4  26308  caures  26364  cnpwstotbnd  26404  ismtyima  26410  rrnmet  26436  reheibor  26446  fnnfpeq0  26637  lzenom  26726  rmxycomplete  26878  fzneg  26945  modabsdifz  26954  jm2.19  26962  pw2f1ocnv  27006  lindfmm  27173  lindsmm  27174  lsslindf  27176  lsslinds  27177  islindf4  27184  caofcan  27416  rfcnpre1  27565  rfcnpre2  27577  pr1eqbg  27952  usg2spot2nb  28176  sbcomwAUX7  29303  sbcomOLD7  29451  sbcom2OLD7  29457  lcvbr  29516  lkrsc  29592  lshpkrlem1  29605  opltcon3b  29699  cmt2N  29745  cmt3N  29746  cvrcon3b  29772  cvrcmp2  29779  cvlexchb2  29826  cvlatexchb2  29830  2llnmj  30054  4atlem3  30090  4atlem9  30097  4atlem10a  30098  4atlem11a  30101  4atlem12a  30104  4at2  30108  2lplnmj  30116  llnexchb2  30363  lautlt  30585  lautcvr  30586  lautco  30591  ltrnatb  30631  ltrneq2  30642  cdlemefrs29pre00  30889  cdlemefrs29cpre1  30892  cdleme32fva  30931  dibglbN  31661  dochsncom  31877  dochkrsat  31950  lspindp5  32265  mapdh8ab  32272  hdmapip0com  32415
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