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  2029  sbcom2  2053  r19.12sn  3696  ordsucelsuc  4613  ordsucsssuc  4614  fvopab3g  5598  fvimacnvALT  5644  respreima  5654  fmptco  5691  fnsuppres  5732  cocan1  5801  cocan2  5802  smoword  6383  oaword  6547  omword  6568  om00el  6574  oeword  6588  nnaword  6625  nnmword  6631  swoer  6688  erth  6704  brecop  6751  eceqoveq  6763  xpdom2  6957  pw2f1olem  6966  omsucdomOLD  7056  fisucdomOLD  7066  ixpfi2  7154  cantnfrescl  7378  rankr1bg  7475  r1pwcl  7519  fseqenlem1  7651  alephord3  7705  alephdom2  7714  engch  8250  fpwwe2lem7  8258  fpwwe2lem9  8260  ltexpi  8526  ltapi  8527  ltmpi  8528  ltsonq  8593  ltmnq  8596  1idpr  8653  addcanpr  8670  axpre-ltadd  8789  axlttri  8894  subsub23  9056  leadd1  9242  ltsub1  9270  ltsub2  9271  leord1  9300  eqord1  9301  lemul1  9608  lediv1  9621  lt2mul2div  9632  lerec  9638  lediv2  9646  le2msq  9656  suprleub  9718  infmrgelb  9734  ofsubeq0  9743  ofsubge0  9745  avgle1  9951  avgle2  9952  cnref1o  10349  xleneg  10545  xltadd1  10576  xsubge0  10581  xposdif  10582  xltmul1  10612  supxrleub  10645  infmxrgelb  10653  iooneg  10756  iccneg  10757  iccsplit  10768  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  fzsplit2  10815  fzaddel  10826  fzrev  10846  elfzo  10877  elfzom1b  10918  negmod0  10979  leexp2  11156  ltexp2r  11158  cjreb  11608  sqrlt  11747  rexfiuz  11831  limsuplt  11953  o1lo1  12011  rlimresb  12039  lo1eq  12042  rlimeq  12043  o1eq  12044  isercoll  12141  efle  12398  tanaddlem  12446  nndivdvds  12537  moddvds  12538  oddm1even  12588  bitsp1  12622  sadcaddlem  12648  sadadd  12658  sadass  12662  bitsshft  12666  smuval2  12673  smumul  12684  dvdssq  12739  phiprmpw  12844  eulerthlem2  12850  odzdvds  12860  pc2dvds  12931  1arith  12974  imasleval  13443  mreacs  13560  catpropd  13612  oppcsect  13676  funcres2b  13771  fthsect  13799  fthinv  13800  fucsect  13846  fucinv  13847  latnlemlt  14190  latnle  14191  ipole  14261  ipolt  14262  spwex  14338  issubg3  14637  eqgid  14669  resghm2b  14701  conjghm  14713  gastacos  14764  resscntz  14807  cntzrec  14809  oppgsubm  14835  oppgsubg  14836  sylow3lem6  14943  lsmcom2  14966  lsmass  14979  lsmcomx  15148  subgdmdprd  15269  opprsubrg  15566  lsslss  15718  lbspropd  15852  islbs2  15907  rspsn  16006  psrbagconf1o  16120  gsumbagdiaglem  16121  mplmonmul  16208  prmirred  16448  znfld  16514  basdif0  16691  restlp  16913  cnrest2  17014  cnprest  17017  cnprest2  17018  lmss  17026  lmff  17029  ist1-2  17075  lpcls  17092  perfcls  17093  cmpfi  17135  hauseqlcld  17340  txlm  17342  txkgen  17346  xkopt  17349  idqtop  17397  tgqtop  17403  qtopcn  17405  uffix  17616  fmco  17656  flimrest  17678  lmflf  17700  txflf  17701  fclsrest  17719  cnpfcf  17736  tsmsgsum  17821  tsmsres  17826  tsmsf1o  17827  ismet2  17898  imasf1oxmet  17939  blres  17977  xmetec  17980  imasf1obl  18034  imasf1oxms  18035  prdsbl  18037  stdbdbl  18063  metrest  18070  tngngp  18170  cnbl0  18283  cnblcld  18284  bl2ioo  18298  cncfcnvcn  18424  iihalf2  18431  icoopnst  18437  iocopnst  18438  icopnfcnv  18440  icopnfhmeo  18441  cphorthcom  18636  caucfil  18709  lmclim  18728  cmsss  18772  volsup  18913  dyaddisjlem  18950  mbfeqalem  18997  mbfeqa  18998  mbfmulc2lem  19002  mbfmax  19004  mbfposr  19007  ismbf3d  19009  mbfimaopnlem  19010  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  0plef  19027  0pledm  19028  i1fmulclem  19057  i1fres  19060  i1fpos  19061  itg1climres  19069  mbfi1fseqlem4  19073  itg2mulclem  19101  itg2monolem1  19105  itg2cnlem1  19116  iblre  19148  iblcn  19153  itgeqa  19168  ellimc2  19227  limcflf  19231  dvreslem  19259  lhop1  19361  ply1remlem  19548  fta1glem2  19552  ofmulrt  19662  plydiveu  19678  plyremlem  19684  quotcan  19689  ulmres  19767  cos11  19895  logleb  19957  argrege0  19965  logdivle  19973  efopn  20005  logccv  20010  cxplt  20041  cxple  20042  cxple2  20044  cxplt2  20045  cxplt3  20047  cxple3  20048  angrtmuld  20106  quad2  20135  atans2  20227  rlimcnp  20260  rlimcnp2  20261  rlimcxp  20268  sqff1o  20420  fsumvma2  20453  dchrptlem2  20504  lgsdilem  20561  lgsne0  20572  lgsqr  20585  lgsquadlem1  20593  lgsquadlem2  20594  m1lgs  20601  dchrisum0lem1  20665  padicabv  20779  rngosn3  21093  nvsubsub23  21220  nmorepnf  21346  blocnilem  21382  ubthlem1  21449  shscom  21898  pjpreeq  21977  spansncol  22147  cmcm2  22195  hodsi  22355  nmoprepnf  22447  nmfnrepnf  22460  pjssposi  22752  cvcon3  22864  mdsymlem8  22990  dmdsym  22993  unipreima  23209  fmptcof2  23229  xrge0iifiso  23317  logblt  23408  indpi1  23605  indf1ofs  23609  subfacp1lem3  23713  subfacp1lem5  23715  eupath2lem3  23903  predfz  24203  elfuns  24454  colinearalglem2  24535  axcgrid  24544  cgrcomr  24620  ofscom  24630  cgr3permute3  24670  cgr3permute1  24671  cgr3com  24676  colinearperm1  24685  colinearperm3  24686  outsideofcom  24751  areacirclem6  24930  areacirc  24931  dupre1  25243  prsubrtr  25399  vtarsuelt  25895  pdiveql  26168  opnbnd  26243  filnetlem4  26330  caures  26476  cnpwstotbnd  26521  ismtyima  26527  rrnmet  26553  reheibor  26563  fnnfpeq0  26758  lzenom  26849  rmxycomplete  27002  fzneg  27069  modabsdifz  27078  jm2.19  27086  pw2f1ocnv  27130  lindfmm  27297  lindsmm  27298  lsslindf  27300  lsslinds  27301  islindf4  27308  caofcan  27540  rfcnpre1  27690  rfcnpre2  27702  usgraeq12d  28111  nbgrasym  28152  lcvbr  29211  lkrsc  29287  lshpkrlem1  29300  opltcon3b  29394  cmt2N  29440  cmt3N  29441  cvrcon3b  29467  cvrcmp2  29474  cvlexchb2  29521  cvlatexchb2  29525  2llnmj  29749  4atlem3  29785  4atlem9  29792  4atlem10a  29793  4atlem11a  29796  4atlem12a  29799  4at2  29803  2lplnmj  29811  llnexchb2  30058  lautlt  30280  lautcvr  30281  lautco  30286  ltrnatb  30326  ltrneq2  30337  cdlemefrs29pre00  30584  cdlemefrs29cpre1  30587  cdleme32fva  30626  dibglbN  31356  dochsncom  31572  dochkrsat  31645  lspindp5  31960  mapdh8ab  31967  hdmapip0com  32110
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