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

Theorem 3bitr4d 298
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 269 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 266 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  fvopab3g  6172  fvimacnvALT  6229  respreima  6237  fmptco  6288  fnnfpeq0  6327  cocan1  6424  cocan2  6425  ordsucelsuc  6891  ordsucsssuc  6892  fnsuppres  7186  smoword  7327  oaword  7493  omword  7514  om00el  7520  oeword  7534  nnaword  7571  nnmword  7577  swoer  7636  erth  7655  brecop  7704  eceqoveq  7717  xpdom2  7917  pw2f1olem  7926  ixpfi2  8124  wemapso2lem  8317  cantnfrescl  8433  rankr1bg  8526  r1pwcl  8570  fseqenlem1  8707  alephord3  8761  alephdom2  8770  engch  9306  fpwwe2lem7  9314  fpwwe2lem9  9316  ltexpi  9580  ltapi  9581  ltmpi  9582  ltsonq  9647  ltmnq  9650  1idpr  9707  addcanpr  9724  axpre-ltadd  9844  axlttri  9960  subsub23  10137  leadd1  10345  ltsub1  10373  ltsub2  10374  leord1  10404  eqord1  10405  lemul1  10724  lediv1  10737  lt2mul2div  10750  lerec  10755  lediv2  10762  le2msq  10772  suprleub  10836  infregelb  10854  ofsubeq0  10864  ofsubge0  10866  avgle1  11119  avgle2  11120  cnref1o  11659  xleneg  11882  xltadd1  11915  xsubge0  11920  xposdif  11921  xltmul1  11951  supxrleub  11984  infxrgelb  11993  iooneg  12119  iccneg  12120  iccsplit  12132  iccshftr  12133  iccshftl  12135  iccdil  12137  icccntr  12139  fzsplit2  12192  fzaddel  12201  fzrev  12228  predfz  12288  elfzo  12296  nelfzo  12299  fzon  12313  elfzom1b  12388  negmod0  12494  leexp2  12732  ltexp2r  12734  repswsymball  13323  repswsymballbi  13324  cjreb  13657  sqrtlt  13796  limsuplt  14004  o1lo1  14062  rlimresb  14090  lo1eq  14093  rlimeq  14094  o1eq  14095  isercoll  14192  efle  14633  tanaddlem  14681  nndivdvds  14773  moddvds  14775  modmulconst  14797  oddm1even  14851  ltoddhalfle  14869  bitsp1  14937  sadcaddlem  14963  sadadd  14973  sadass  14977  bitsshft  14981  smuval2  14988  smumul  14999  dvdssq  15064  phiprmpw  15265  eulerthlem2  15271  odzdvds  15284  pc2dvds  15367  1arith  15415  imasleval  15970  mreacs  16088  catpropd  16138  oppcsect  16207  funcres2b  16326  fthsect  16354  fthinv  16355  fucsect  16401  fucinv  16402  latnlemlt  16853  latnle  16854  ipole  16927  ipolt  16928  issubg3  17381  eqgid  17415  resghm2b  17447  conjghm  17460  gastacos  17512  resscntz  17533  cntzrec  17535  oppgsubm  17561  oppgsubg  17562  sylow3lem6  17816  lsmcom2  17839  lsmass  17852  ablsubsub23  17999  lsmcomx  18028  subgdmdprd  18202  opprsubrg  18570  lsslss  18728  lbspropd  18866  islbs2  18921  rspsn  19021  psrbagconf1o  19141  gsumbagdiaglem  19142  mplmonmul  19231  prmirred  19607  znfld  19673  lindfmm  19927  lindsmm  19928  lsslindf  19930  lsslinds  19931  islindf4  19938  basdif0  20510  neiptopreu  20689  neitr  20736  restlp  20739  cnrest2  20842  cnprest  20845  cnprest2  20846  lmss  20854  lmff  20857  ist1-2  20903  lpcls  20920  perfcls  20921  cmpfi  20963  hauseqlcld  21201  txlm  21203  txkgen  21207  xkopt  21210  idqtop  21261  tgqtop  21267  qtopcn  21269  uffix  21477  fmco  21517  flimrest  21539  lmflf  21561  txflf  21562  fclsrest  21580  cnpfcf  21597  tsmsgsum  21694  tsmsres  21699  tsmsf1o  21700  fmucndlem  21847  ismet2  21889  imasf1oxmet  21931  blres  21987  xmetec  21990  imasf1obl  22044  imasf1oxms  22045  prdsbl  22047  stdbdbl  22073  metrest  22080  metustsym  22111  blval2  22118  metuel2  22121  tngngp  22206  cnbl0  22319  cnblcld  22320  bl2ioo  22335  cncfcnvcn  22463  iihalf2  22471  icoopnst  22477  iocopnst  22478  icopnfcnv  22480  icopnfhmeo  22481  cphorthcom  22732  caucfil  22807  lmclim  22826  cmsss  22872  rrxmet  22916  volsup  23048  dyaddisjlem  23086  mbfeqalem  23132  mbfeqa  23133  mbfmulc2lem  23137  mbfmax  23139  mbfposr  23142  ismbf3d  23144  mbfimaopnlem  23145  mbfaddlem  23150  mbfsup  23154  mbfinf  23155  0plef  23162  0pledm  23163  i1fmulclem  23192  i1fres  23195  i1fpos  23196  itg1climres  23204  mbfi1fseqlem4  23208  itg2mulclem  23236  itg2monolem1  23240  itg2cnlem1  23251  iblre  23283  iblcn  23288  itgeqa  23303  ellimc2  23364  limcflf  23368  dvreslem  23396  lhop1  23498  ply1remlem  23643  fta1glem2  23647  ofmulrt  23758  plydiveu  23774  plyremlem  23780  quotcan  23785  ulmres  23863  cos11  24000  logleb  24070  argrege0  24078  logdivle  24089  efopn  24121  logccv  24126  cxplt  24157  cxple  24158  cxple2  24160  cxplt2  24161  cxplt3  24163  cxple3  24164  logbleb  24238  logblt  24239  angrtmuld  24255  quad2  24283  atans2  24375  rlimcnp  24409  rlimcnp2  24410  rlimcxp  24417  sqff1o  24625  fsumvma2  24656  dchrptlem2  24707  lgsdilem  24766  lgsne0  24777  lgsqr  24793  lgsquadlem1  24822  lgsquadlem2  24823  m1lgs  24830  2lgslem1a  24833  2lgs  24849  dchrisum0lem1  24922  padicabv  25036  trgcgrg  25128  colcom  25171  colrot1  25172  ishlg  25215  hlcomb  25216  hlbtwn  25224  lncom  25235  lnrot2  25237  israg  25310  perpcom  25326  hpgcom  25377  colopp  25379  iscgra  25419  isinag  25447  colinearalglem2  25505  axcgrid  25514  uhgraeq12d  25602  usgraeq12d  25657  nbgrasym  25734  cusgrauvtxb  25790  usg2wlkeq  26002  clwlkisclwwlk  26083  eupath2lem3  26272  usg2spot2nb  26358  nvsubsub23  26687  nmorepnf  26813  blocnilem  26849  ubthlem1  26916  shscom  27368  pjpreeq  27447  spansncol  27617  cmcm2  27665  hodsi  27824  nmoprepnf  27916  nmfnrepnf  27929  pjssposi  28221  cvcon3  28333  mdsymlem8  28459  dmdsym  28462  disjunsn  28595  fimarab  28631  unipreima  28632  fmptcof2  28645  1stpreima  28673  fpwrelmapffslem  28701  infxrge0gelb  28727  nndiffz1  28742  isinftm  28872  metidv  29069  metider  29071  pstmxmet  29074  xrge0iifiso  29115  indpi1  29217  indf1ofs  29221  aean  29440  brfae  29444  signsply0  29760  signsvfn  29791  subfacp1lem3  30224  subfacp1lem5  30226  opelco3  30729  sscoid  30996  cgrcomr  31080  ofscom  31090  cgr3permute3  31130  cgr3permute1  31131  cgr3com  31136  colinearperm1  31145  colinearperm3  31146  outsideofcom  31211  opnbnd  31296  filnetlem4  31352  finxpsuclem  32206  wl-equsald  32300  wl-sbcom3  32347  poimirlem23  32398  broucube  32409  heicant  32410  itg2addnclem2  32428  ftc1anclem1  32451  ftc1anclem5  32455  ftc1anclem6  32456  areacirclem5  32470  areacirc  32471  caures  32522  cnpwstotbnd  32562  ismtyima  32568  rrnmet  32594  reheibor  32604  rngosn3  32689  lcvbr  33122  lkrsc  33198  lshpkrlem1  33211  opltcon3b  33305  cmt2N  33351  cmt3N  33352  cvrcon3b  33378  cvrcmp2  33385  cvlexchb2  33432  cvlatexchb2  33436  2llnmj  33660  4atlem3  33696  4atlem9  33703  4atlem10a  33704  4atlem11a  33707  4atlem12a  33710  4at2  33714  2lplnmj  33722  llnexchb2  33969  lautlt  34191  lautcvr  34192  lautco  34197  ltrnatb  34237  ltrneq2  34248  cdlemefrs29pre00  34497  cdlemefrs29cpre1  34500  cdleme32fva  34539  dibglbN  35269  dochsncom  35485  dochkrsat  35558  lspindp5  35873  mapdh8ab  35880  hdmapip0com  36023  lzenom  36147  rmxycomplete  36296  fzneg  36363  modabsdifz  36367  jm2.19  36374  pw2f1ocnv  36418  brtrclfv2  36834  rfovcnvf1od  37114  ntrclsfveq1  37174  ntrclsiso  37181  k0004lem2  37262  caofcan  37340  rfcnpre1  37997  rfcnpre2  38009  ellimcabssub0  38481  fperdvper  38605  vonvolmbl  39348  pr1eqbg  40111  nbgrsym  40586  uvtxa01vtx0  40618  iscplgredg  40634  rgrusgrprc  40784  uspgr2wlkeq  40849  clwlkclwwlk  41206  eupth2lem3lem6  41396  fusgr2wsp2nb  41493  mgmpropd  41560  lco0  42005  lindslininds  42042  ltsubaddb  42093  ltsubsubb  42094  ltsubadd2b  42095  elbigolo1  42144  dig2bits  42201
  Copyright terms: Public domain W3C validator