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

Theorem 3imtr4d 282
Description: More general version of 3imtr4i 280. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)
Hypotheses
Ref Expression
3imtr4d.1 (𝜑 → (𝜓𝜒))
3imtr4d.2 (𝜑 → (𝜃𝜓))
3imtr4d.3 (𝜑 → (𝜏𝜒))
Assertion
Ref Expression
3imtr4d (𝜑 → (𝜃𝜏))

Proof of Theorem 3imtr4d
StepHypRef Expression
1 3imtr4d.2 . 2 (𝜑 → (𝜃𝜓))
2 3imtr4d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3imtr4d.3 . . 3 (𝜑 → (𝜏𝜒))
42, 3sylibrd 248 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbid 229 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  unielrel  5577  predpo  5615  fvrnressn  6333  fconst5  6376  soisores  6477  caofrss  6828  caoftrn  6830  f1o2ndf1  7172  oaord  7514  omord2  7534  omcan  7536  oeord  7555  oecan  7556  nnaord  7586  nnmord  7599  omsmo  7621  pmss12g  7770  cantnf  8473  pm54.43  8709  ttukeylem2  9215  axlttrn  9989  axltadd  9990  axmulgt0  9991  axsup  9992  ltadd2  10020  ltord1  10433  recex  10538  prodge0  10749  ltmul1  10752  lt2msq  10787  nnge1  10923  zltp1le  11304  uzss  11584  eluzp1m1  11587  ixxssixx  12060  zesq  12849  swrdccatin12lem3  13341  swrdccat3blem  13346  relexpsucnnr  13613  climrlim2  14126  rlimres  14137  climshftlem  14153  lo1add  14205  lo1mul  14206  rlimsqzlem  14227  lo1le  14230  isercolllem2  14244  isercoll  14246  climsup  14248  cvgcmp  14389  climcndslem1  14420  dvds1lem  14831  sumodd  14949  algcvg  15127  eucalgcvga  15137  rpexp12i  15272  crth  15321  pc2dvds  15421  pcmpt  15434  prmpwdvds  15446  1arith  15469  vdwlem2  15524  vdwlem6  15528  vdwlem8  15530  ercpbl  16032  initoid  16478  termoid  16479  ipopos  16983  subginv  17424  symggrp  17643  f1otrspeq  17690  lsmless1x  17882  lsmless2x  17883  dprdss  18251  dvdsunit  18486  irredrmul  18530  isdrngd  18595  lspextmo  18877  evlseu  19337  domnchr  19699  zntoslem  19724  mat2pmatf1  20353  tgss  20583  neips  20727  opnnei  20734  lpss3  20758  ssrest  20790  t1t0  20962  kgen2ss  21168  isfild  21472  fgss  21487  fgss2  21488  cnpflf2  21614  fclsss1  21636  fclsss2  21637  tgpt0  21732  tsmsxp  21768  prdsxmslem2  22144  ngptgp  22250  nghmcn  22359  qdensere  22383  evth  22566  nmhmcn  22728  tchcph  22844  caussi  22903  equivcfil  22905  rrxmvallem  22995  ivthlem2  23028  ovollb2lem  23063  ovolunlem1  23072  volun  23120  ioombl1lem4  23136  volsup2  23179  volcn  23180  ismbf3d  23227  itg2mulclem  23319  cpnord  23504  lhop1  23581  aaliou3lem2  23902  ulmclm  23945  ulmss  23955  abelth  23999  cosord  24082  efif1olem4  24095  argimgt0  24162  logdivlt  24171  cxploglim  24504  dvdssqf  24664  mumullem1  24705  mumullem2  24706  bposlem6  24814  lgsdchr  24880  gausslemma2dlem1a  24890  m1lgs  24913  chtppilim  24964  ax5seg  25618  axpasch  25621  axlowdimlem16  25637  axeuclid  25643  axcontlem4  25647  elusuhgra  25897  nb3gra2nb  25984  spthispth  26103  wlkdvspth  26138  cycliscrct  26158  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  cusconngra  26204  erclwwlknsym  26354  erclwwlkntr  26355  clwlkfclwwlk  26371  eupatrl  26495  frgra3vlem1  26527  3vfriswmgralem  26531  frgrawopreglem2  26572  usg2spot2nb  26592  2spotmdisj  26595  numclwwlk5  26639  minvecolem5  27121  ocsh  27526  shless  27602  leopadd  28375  leopmuli  28376  leopmul2i  28378  leoptr  28380  spansncv2  28536  mdsl0  28553  ssdmd1  28556  cvdmd  28580  cdj3i  28684  cmpcref  29245  cvmliftmolem1  30517  mrsubff1  30665  msubff1  30707  lediv2aALT  30825  nodenselem5  31084  cgr3tr4  31329  colinearxfr  31352  lineext  31353  brsegle  31385  seglecgr12im  31387  segletr  31391  colinbtwnle  31395  outsideoftr  31406  lineelsb2  31425  ivthALT  31500  tailfb  31542  poimirlem29  32608  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  incsequz  32714  mettrifi  32723  ismtycnv  32771  bfplem1  32791  ghomco  32860  rngoisocnv  32950  keridl  33001  dmncan1  33045  ax12indalem  33248  ax12inda2ALT  33249  omllaw4  33551  cmtcomlemN  33553  cvlexch2  33634  cvlatexch2  33642  cvrexch  33724  atexchltN  33745  3atlem5  33791  lplnribN  33855  linepsubN  34056  paddss1  34121  paddss2  34122  pmapjoin  34156  pmapjat1  34157  cdleme36a  34766  dib2dim  35550  dih2dimbALTN  35552  djhcvat42  35722  dihjatcclem4  35728  dihjat1lem  35735  lcfrlem6  35854  hlhillcs  36268  pell1234qrmulcl  36437  pell14qrss1234  36438  pell14qrmulcl  36445  pell14qrreccl  36446  pell1qrss14  36450  monotoddzzfi  36525  oddcomabszz  36527  climinf  38673  iccpartgt  39965  2ffzoeq  40361  usgr1v0e  40545  nb3gr2nb  40612  cplgr1v  40652  wlk1wlk  40846  sPthisPth  40932  usgr2pthlem  40969  cyclisCrct  41005  erclwwlksnsym  41254  erclwwlksntr  41255  clwlksfclwwlk  41269  frgr3vlem1  41443  3vfriswmgrlem  41447  av-numclwwlk5  41542
  Copyright terms: Public domain W3C validator