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

Theorem 3bitr4d 300
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 (𝜑 → (𝜓𝜒))
3bitr4d.2 (𝜑 → (𝜃𝜓))
3bitr4d.3 (𝜑 → (𝜏𝜒))
Assertion
Ref Expression
3bitr4d (𝜑 → (𝜃𝜏))

Proof of Theorem 3bitr4d
StepHypRef Expression
1 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
2 3bitr4d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3bitr4d.3 . . 3 (𝜑 → (𝜏𝜒))
42, 3bitr4d 271 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 268 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  pr1eqbg  4521  fvopab3g  6419  fvimacnvALT  6479  respreima  6487  fmptco  6539  fnnfpeq0  6588  cocan1  6689  cocan2  6690  ordsucelsuc  7169  ordsucsssuc  7170  fnsuppres  7474  smoword  7616  oaword  7783  omword  7804  om00el  7810  oeword  7824  nnaword  7861  nnmword  7867  swoer  7926  erth  7943  brecop  7992  eceqoveq  8005  xpdom2  8211  pw2f1olem  8220  ixpfi2  8420  wemapso2lem  8613  cantnfrescl  8737  rankr1bg  8830  r1pwcl  8874  fseqenlem1  9047  alephord3  9101  alephdom2  9110  engch  9652  fpwwe2lem7  9660  fpwwe2lem9  9662  ltexpi  9926  ltapi  9927  ltmpi  9928  ltsonq  9993  ltmnq  9996  1idpr  10053  addcanpr  10070  axpre-ltadd  10190  axlttri  10311  subsub23  10488  leadd1  10698  ltsub1  10726  ltsub2  10727  leord1  10757  eqord1  10758  lemul1  11077  lediv1  11090  lt2mul2div  11103  lerec  11108  lediv2  11115  le2msq  11125  suprleub  11191  infregelb  11209  ofsubeq0  11219  ofsubge0  11221  avgle1  11474  avgle2  11475  cnref1o  12030  xleneg  12254  xltadd1  12291  xsubge0  12296  xposdif  12297  xltmul1  12327  supxrleub  12361  infxrgelb  12370  iooneg  12499  iccneg  12500  iccsplit  12512  iccshftr  12513  iccshftl  12515  iccdil  12517  icccntr  12519  fzsplit2  12573  fzaddel  12582  fzrev  12610  predfz  12672  elfzo  12680  nelfzo  12683  fzon  12697  elfzom1b  12775  negmod0  12885  leexp2  13122  ltexp2r  13124  repswsymball  13735  repswsymballbi  13736  cjreb  14071  sqrtlt  14210  limsuplt  14418  o1lo1  14476  rlimresb  14504  lo1eq  14507  rlimeq  14508  o1eq  14509  isercoll  14606  efle  15054  tanaddlem  15102  nndivdvds  15198  moddvds  15200  modmulconst  15222  oddm1even  15275  ltoddhalfle  15293  bitsp1  15361  sadcaddlem  15387  sadadd  15397  sadass  15401  bitsshft  15405  smuval2  15412  smumul  15423  dvdssq  15488  phiprmpw  15688  eulerthlem2  15694  odzdvds  15707  pc2dvds  15790  1arith  15838  imasleval  16409  mreacs  16526  catpropd  16576  oppcsect  16645  funcres2b  16764  fthsect  16792  fthinv  16793  fucsect  16839  fucinv  16840  latnlemlt  17292  latnle  17293  ipole  17366  ipolt  17367  issubg3  17820  eqgid  17854  resghm2b  17886  conjghm  17899  gastacos  17950  resscntz  17971  cntzrec  17973  oppgsubm  17999  oppgsubg  18000  sylow3lem6  18254  lsmcom2  18277  lsmass  18290  ablsubsub23  18437  lsmcomx  18466  subgdmdprd  18641  opprsubrg  19011  lsslss  19174  lbspropd  19312  islbs2  19369  rspsn  19469  psrbagconf1o  19589  gsumbagdiaglem  19590  mplmonmul  19679  prmirred  20058  znfld  20124  lindfmm  20383  lindsmm  20384  lsslindf  20386  lsslinds  20387  islindf4  20394  basdif0  20978  neiptopreu  21158  neitr  21205  restlp  21208  cnrest2  21311  cnprest  21314  cnprest2  21315  lmss  21323  lmff  21326  ist1-2  21372  lpcls  21389  perfcls  21390  cmpfi  21432  hauseqlcld  21670  txlm  21672  txkgen  21676  xkopt  21679  idqtop  21730  tgqtop  21736  qtopcn  21738  uffix  21945  fmco  21985  flimrest  22007  lmflf  22029  txflf  22030  fclsrest  22048  cnpfcf  22065  tsmsgsum  22162  tsmsres  22167  tsmsf1o  22168  fmucndlem  22315  ismet2  22358  imasf1oxmet  22400  blres  22456  xmetec  22459  imasf1obl  22513  imasf1oxms  22514  prdsbl  22516  stdbdbl  22542  metrest  22549  metustsym  22580  blval2  22587  metuel2  22590  tngngp  22678  cnbl0  22797  cnblcld  22798  bl2ioo  22815  cncfcnvcn  22944  iihalf2  22952  icoopnst  22958  iocopnst  22959  icopnfcnv  22961  icopnfhmeo  22962  cphorthcom  23220  caucfil  23300  lmclim  23320  cmsss  23366  rrxmet  23410  volsup  23544  dyaddisjlem  23583  mbfeqalem  23629  mbfeqa  23630  mbfmulc2lem  23634  mbfmax  23636  mbfposr  23639  ismbf3d  23641  mbfimaopnlem  23642  mbfaddlem  23647  mbfsup  23651  mbfinf  23652  0plef  23659  0pledm  23660  i1fmulclem  23689  i1fres  23692  i1fpos  23693  itg1climres  23701  mbfi1fseqlem4  23705  itg2mulclem  23733  itg2monolem1  23737  itg2cnlem1  23748  iblre  23780  iblcn  23785  itgeqa  23800  ellimc2  23861  limcflf  23865  dvreslem  23893  lhop1  23997  ply1remlem  24142  fta1glem2  24146  ofmulrt  24257  plydiveu  24273  plyremlem  24279  quotcan  24284  ulmres  24362  cos11  24500  logleb  24570  argrege0  24578  logdivle  24589  efopn  24625  logccv  24630  cxplt  24661  cxple  24662  cxple2  24664  cxplt2  24665  cxplt3  24667  cxple3  24668  logbleb  24742  logblt  24743  angrtmuld  24759  quad2  24787  atans2  24879  rlimcnp  24913  rlimcnp2  24914  rlimcxp  24921  sqff1o  25129  fsumvma2  25160  dchrptlem2  25211  lgsdilem  25270  lgsne0  25281  lgsqr  25297  lgsquadlem1  25326  lgsquadlem2  25327  m1lgs  25334  2lgslem1a  25337  2lgs  25353  dchrisum0lem1  25426  padicabv  25540  trgcgrg  25631  colcom  25674  colrot1  25675  ishlg  25718  hlcomb  25719  hlbtwn  25727  lncom  25738  lnrot2  25740  israg  25813  perpcom  25829  hpgcom  25880  colopp  25882  iscgra  25922  isinag  25950  colinearalglem2  26008  axcgrid  26017  nbgrsymOLD  26487  uvtx01vtx  26525  uvtxa01vtx0OLD  26527  iscplgredg  26548  rgrusgrprc  26720  uspgr2wlkeq  26777  clwlkclwwlk  27152  eupth2lem3lem6  27413  fusgr2wsp2nb  27516  nmorepnf  27963  blocnilem  27999  ubthlem1  28066  shscom  28518  pjpreeq  28597  spansncol  28767  cmcm2  28815  hodsi  28974  nmoprepnf  29066  nmfnrepnf  29079  pjssposi  29371  cvcon3  29483  mdsymlem8  29609  dmdsym  29612  disjunsn  29745  fimarab  29785  unipreima  29786  fmptcof2  29797  1stpreima  29824  fpwrelmapffslem  29847  infxrge0gelb  29871  nndiffz1  29888  isinftm  30075  metidv  30275  metider  30277  pstmxmet  30280  xrge0iifiso  30321  indpi1  30422  prodindf  30425  indf1ofs  30428  aean  30647  brfae  30651  signsply0  30968  signsvfn  30999  reprinrn  31036  subfacp1lem3  31502  subfacp1lem5  31504  opelco3  32014  sscoid  32357  cgrcomr  32441  ofscom  32451  cgr3permute3  32491  cgr3permute1  32492  cgr3com  32497  colinearperm1  32506  colinearperm3  32507  outsideofcom  32572  opnbnd  32657  filnetlem4  32713  finxpsuclem  33571  wl-equsald  33660  poimirlem23  33765  broucube  33776  heicant  33777  itg2addnclem2  33794  ftc1anclem1  33817  ftc1anclem5  33821  ftc1anclem6  33822  areacirclem5  33836  areacirc  33837  caures  33888  cnpwstotbnd  33928  ismtyima  33934  rrnmet  33960  reheibor  33970  rngosn3  34055  brcosscnvcoss  34531  br1cosscnvxrn  34566  lcvbr  34830  lkrsc  34906  lshpkrlem1  34919  opltcon3b  35013  cmt2N  35059  cmt3N  35060  cvrcon3b  35086  cvrcmp2  35093  cvlexchb2  35140  cvlatexchb2  35144  2llnmj  35368  4atlem3  35404  4atlem9  35411  4atlem10a  35412  4atlem11a  35415  4atlem12a  35418  4at2  35422  2lplnmj  35430  llnexchb2  35677  lautlt  35899  lautcvr  35900  lautco  35905  ltrnatb  35945  ltrneq2  35956  cdlemefrs29pre00  36204  cdlemefrs29cpre1  36207  cdleme32fva  36246  dibglbN  36976  dochsncom  37192  dochkrsat  37265  lspindp5  37580  mapdh8ab  37587  hdmapip0com  37727  lzenom  37859  rmxycomplete  38008  fzneg  38075  modabsdifz  38079  jm2.19  38086  pw2f1ocnv  38130  brtrclfv2  38545  rfovcnvf1od  38824  ntrclsfveq1  38884  ntrclsiso  38891  k0004lem2  38972  caofcan  39048  rfcnpre1  39700  rfcnpre2  39712  ellimcabssub0  40367  fperdvper  40651  vonvolmbl  41395  mgmpropd  42303  lco0  42744  lindslininds  42781  ltsubaddb  42832  ltsubsubb  42833  ltsubadd2b  42834  elbigolo1  42879  dig2bits  42936
  Copyright terms: Public domain W3C validator