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

Theorem 3imp 1255
Description: Importation inference. (Contributed by NM, 8-Apr-1994.)
Hypothesis
Ref Expression
3imp.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
3imp ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3imp
StepHypRef Expression
1 df-3an 1039 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 448 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3sylbi 207 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037
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  df-an 386  df-3an 1039
This theorem is referenced by:  3imp31  1256  3imp231  1257  3impa  1258  3impb  1259  3impia  1260  3impib  1261  3com23  1270  3imp21  1276  3an1rs  1278  3imp1  1279  3impd  1280  syl3an2  1359  syl3an3  1360  3jao  1388  biimp3ar  1432  3elpr2eq  4433  wefrc  5106  predpo  5696  f1ssf1  6166  fveqdmss  6352  poxp  7286  fvn0elsuppb  7309  smo11  7458  odi  7656  omass  7657  nndi  7700  nnmass  7701  undifixp  7941  isinf  8170  domunfican  8230  infssuni  8254  pr2nelem  8824  dfac8alem  8849  fin33i  9188  fin1a2lem10  9228  domtriomlem  9261  axdc3lem2  9270  axdc3lem4  9272  axdc4lem  9274  ttukeyg  9336  axdclem  9338  grupr  9616  nqereu  9748  squeeze0  10923  rpnnen1lem5  11815  rpnnen1lem5OLD  11821  xnn0lenn0nn0  12072  supxrun  12143  difelfzle  12448  elfzo0z  12505  fzofzim  12510  fzo1fzo0n0  12514  elfzodifsumelfzo  12529  elfznelfzo  12569  injresinj  12584  mulexp  12894  expadd  12897  expmul  12900  bernneq  12985  facdiv  13069  hashgt12el2  13206  hashimarni  13223  leisorel  13239  fi1uzind  13274  fi1uzindOLD  13280  2swrd1eqwrdeq  13448  swrdswrdlem  13453  swrdccat3  13486  swrdccatid  13491  repswswrd  13525  cshf1  13550  2cshwcshw  13565  cshimadifsn  13569  swrdco  13577  relexpindlem  13797  dvdsaddre2b  15023  addmodlteqALT  15041  ltoddhalfle  15079  halfleoddlt  15080  dfgcd2  15257  coprmprod  15369  coprmproddvds  15371  cncongr1  15375  oddprmgt2  15405  prmfac1  15425  infpnlem1  15608  prmgaplem5  15753  prmgaplem6  15754  cshwshashlem1  15796  setsstruct  15892  iscatd2  16336  initoeu2lem2  16659  clatleglb  17120  dfgrp3e  17509  mulgaddcom  17558  mulginvcom  17559  symgfvne  17802  f1rhm0to0ALT  18735  lmodvsmmulgdi  18892  lsmcv  19135  assamulgscm  19344  psrvscafval  19384  mamufacex  20189  mat1scmat  20339  gsummatr01lem4  20458  cramer0  20490  chpscmat  20641  fvmptnn04ifa  20649  fvmptnn04ifc  20651  fvmptnn04ifd  20652  fiinopn  20700  opnneissb  20912  cnpimaex  21054  regsep  21132  hausnei2  21151  cmpsublem  21196  cmpsub  21197  filufint  21718  blssps  22223  blss  22224  mblsplit  23294  bcmono  24996  gausslemma2dlem1a  25084  2sqlem10  25147  upgrex  25981  numedglnl  26033  ausgrumgri  26056  ausgrusgri  26057  usgredg2vtxeuALT  26108  ushgredgedg  26115  ushgredgedgloop  26117  edg0usgr  26139  0uhgrsubgr  26165  subumgredg2  26171  fusgrfisbase  26214  cusgrsizeinds  26342  cusgrsize2inds  26343  finsumvtxdg2size  26440  upgrewlkle2  26496  wlkl1loop  26528  pthdivtx  26619  2pthnloop  26621  upgrwlkdvde  26627  uhgrwkspthlem2  26644  usgr2pthlem  26653  usgr2pth  26654  clwlkl1loop  26672  crctcshwlkn0lem4  26699  wwlksnextproplem3  26800  umgr2adedgwlkonALT  26837  umgr2wlk  26839  umgr2wlkon  26840  elwwlks2  26855  clwlkclwwlklem2  26895  umgrclwwlksge2  26905  clwwlksel  26907  clwwlksext2edg  26916  clwwnisshclwwsn  26923  1pthon2v  27006  uhgr3cyclex  27035  eupth2lem3lem6  27086  frgr3vlem1  27130  3cyclfrgrrn1  27142  frgrnbnb  27150  frgrwopreglem5  27171  numclwwlkovf2ex  27204  extwwlkfab  27207  numclwlk1lem2foa  27208  frgrregord013  27237  frgrregord13  27238  frgrogt3nreg  27239  friendship  27241  chcompl  28083  spansncol  28411  hoaddsub  28659  bnj600  30974  sconnpht  31196  msubvrs  31442  funpsstri  31649  imp5p  32289  cntotbnd  33575  clmgmOLD  33630  grpomndo  33654  rngoneglmul  33722  rngonegrmul  33723  zerdivemp1x  33726  atlex  34429  cvlexch1  34441  cvlsupr4  34458  cvlsupr5  34459  cvlsupr6  34460  2llnneN  34521  athgt  34568  llnle  34630  lplnle  34652  lvoli2  34693  pmaple  34873  dalawlem10  34992  dalawlem13  34995  dalawlem14  34996  dalaw  34998  lhp2lt  35113  ldilval  35225  cdleme50trn2  35665  cdlemf  35677  cdlemg18b  35793  tendotp  35875  tendospcanN  36138  dihmeetlem3N  36420  dvh4dimlem  36558  pell14qrexpclnn0  37256  pell1qrgap  37264  aomclem2  37451  rngunsnply  37569  relexpxpmin  37835  relexpaddss  37836  rp-simp2  37913  gneispaceel2  38268  bi33imp12  38522  bi23imp13  38523  bi13imp23  38524  bi23imp1  38527  bi123imp0  38528  ee333  38539  jaoded  38608  e333  38786  suctrALTcf  38984  suctrALTcfVD  38985  ax6e2ndeqALT  38993  mullimc  39654  mullimcf  39661  fzopredsuc  41102  subsubelfzo0  41105  iccpartimp  41123  iccpartigtl  41129  lswn0  41150  pfxfv  41170  pfxccat3  41197  reuccatpfxs1lem  41204  fmtnofac1  41253  pwdif  41272  lighneallem2  41294  lighneallem3  41295  lighneallem4  41298  mogoldbblem  41400  gbegt5  41420  sbgoldbaltlem1  41438  bgoldbtbndlem2  41465  bgoldbtbndlem3  41466  lidldomn1  41692  cznnring  41727  rngccatidALTV  41760  ringccatidALTV  41823  scmsuppss  41924  lmodvsmdi  41934  gsumlsscl  41935  lindslinindimp2lem1  42018  lindsrng01  42028  elfzolborelfzop1  42080  difmodm1lt  42088  fllog2  42133  dignn0flhalflem1  42180
  Copyright terms: Public domain W3C validator