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

Theorem 3imp 1112
Description: Importation inference. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jun-2022.)
Hypothesis
Ref Expression
3imp.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
3imp ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3imp
StepHypRef Expression
1 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21imp31 419 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1111 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  3imp31  1113  3imp231  1114  3impb  1116  3impib  1117  3imp1  1348  3impd  1349  3jao  1426  biimp3ar  1471  3elpr2eq  4865  wefrc  5628  iotan0  6487  f1ssf1  6817  fveqdmss  7030  funelss  7980  poxp  8061  fvn0elsuppb  8113  suppfnss  8121  smo11  8311  odi  8527  omass  8528  nndi  8571  nnmass  8572  undifixp  8873  domunfican  9265  preleqg  9552  pr2nelemOLD  9940  dfac8alem  9966  fin33i  10306  domtriomlem  10379  axdc3lem2  10388  axdc3lem4  10390  axdc4lem  10392  ttukeyg  10454  axdclem  10456  grupr  10734  nqereu  10866  squeeze0  12059  rpnnen1lem5  12907  xnn0lenn0nn0  13165  supxrun  13236  difelfzle  13555  elfzo0z  13615  fzofzim  13620  fzo1fzo0n0  13624  elfzodifsumelfzo  13639  elfznelfzo  13678  injresinj  13694  mulexp  14008  expadd  14011  expmul  14014  facdiv  14188  hashgt12el2  14324  hashimarni  14342  leisorel  14360  fi1uzind  14397  pfxfv  14571  swrdswrdlem  14593  pfxccat3  14623  reuccatpfxs1lem  14635  repswswrd  14673  cshf1  14699  2cshwcshw  14715  cshimadifsn  14719  relexpindlem  14949  pwdif  15754  dvdsaddre2b  16190  addmodlteqALT  16208  ltoddhalfle  16244  halfleoddlt  16245  coprmprod  16538  coprmproddvds  16540  cncongr1  16544  oddprmgt2  16576  prmfac1  16598  infpnlem1  16783  prmgaplem5  16928  prmgaplem6  16929  cshwshashlem1  16969  setsstruct  17049  iscatd2  17562  initoeu2lem2  17902  clatleglb  18408  dfgrp3e  18848  mulgaddcom  18901  mulginvcom  18902  symgfvne  19163  f1rhm0to0ALT  20176  lsmcv  20605  assamulgscm  21307  psrvscafval  21361  mat1scmat  21891  cramer0  22042  chpscmat  22194  fvmptnn04ifa  22202  fvmptnn04ifc  22204  fvmptnn04ifd  22205  fiinopn  22253  opnneissb  22468  cnpimaex  22610  regsep  22688  hausnei2  22707  cmpsublem  22753  cmpsub  22754  filufint  23274  blssps  23780  blss  23781  mblsplit  24899  bcmono  26628  gausslemma2dlem1a  26716  2sqlem10  26779  addsunif  27313  negsunif  27353  elntg2  27937  upgrex  28046  numedglnl  28098  ausgrumgri  28121  ausgrusgri  28122  usgredg2vtxeuALT  28173  ushgredgedg  28180  ushgredgedgloop  28182  edg0usgr  28204  0uhgrsubgr  28230  subumgredg2  28236  fusgrfisbase  28279  cusgrsizeinds  28403  cusgrsize2inds  28404  finsumvtxdg2size  28501  upgrewlkle2  28557  wlkl1loop  28589  pthdivtx  28680  2pthnloop  28682  upgrwlkdvde  28688  uhgrwkspthlem2  28705  usgr2pthlem  28714  usgr2pth  28715  clwlkl1loop  28734  crctcshwlkn0lem4  28761  wwlksnextproplem3  28859  wspn0  28872  umgr2adedgwlkonALT  28895  umgr2wlk  28897  umgr2wlkon  28898  elwwlks2  28914  clwwlkccatlem  28936  umgrclwwlkge2  28938  clwlkclwwlklem2  28947  clwlkclwwlkf1lem2  28952  clwlkclwwlkf  28955  clwwlknlbonbgr1  28986  clwwlkn1loopb  28990  clwwlkel  28993  clwwlkext2edg  29003  clwwlknonex2lem2  29055  clwwlknonex2  29056  clwwlknonex2e  29057  1pthon2v  29100  uhgr3cyclex  29129  eupth2lem3lem6  29180  frgr3vlem1  29220  3cyclfrgrrn1  29232  frgrnbnb  29240  frgrwopreglem4a  29257  2clwwlk2clwwlklem  29293  wlkl0  29314  frgrregord013  29342  frgrregord13  29343  frgrogt3nreg  29344  friendship  29346  chcompl  30187  spansncol  30513  hoaddsub  30761  bnj600  33534  sconnpht  33826  satffunlem  33998  satfvel  34009  msubvrs  34157  funpsstri  34343  imp5p  34786  cntotbnd  36258  clmgmOLD  36313  grpomndo  36337  rngoneglmul  36405  rngonegrmul  36406  zerdivemp1x  36409  atlex  37781  cvlexch1  37793  cvlsupr4  37810  cvlsupr5  37811  cvlsupr6  37812  2llnneN  37875  athgt  37922  llnle  37984  lplnle  38006  lvoli2  38047  pmaple  38227  dalawlem10  38346  dalawlem13  38349  dalawlem14  38350  dalaw  38352  lhp2lt  38467  ldilval  38579  cdleme50trn2  39017  cdlemf  39029  cdlemg18b  39145  tendotp  39227  tendospcanN  39489  dihmeetlem3N  39771  dvh4dimlem  39909  pell14qrexpclnn0  41192  pell1qrgap  41200  aomclem2  41385  rngunsnply  41503  dflim5  41666  relexpaddss  41997  rp-simp2  42072  gneispaceel2  42423  bi33imp12  42779  bi23imp13  42780  bi13imp23  42781  bi23imp1  42784  bi123imp0  42785  ee333  42796  jaoded  42855  e333  43022  suctrALTcf  43211  suctrALTcfVD  43212  ax6e2ndeqALT  43220  mullimc  43864  mullimcf  43871  f1oresf1o2  45530  fzopredsuc  45562  subsubelfzo0  45565  elsetpreimafvbi  45590  iccpartimp  45616  iccpartigtl  45622  lswn0  45643  poprelb  45723  fmtnofac1  45769  lighneallem2  45805  lighneallem3  45806  lighneallem4  45809  mogoldbblem  45919  fpprel2  45940  gbegt5  45960  sbgoldbaltlem1  45978  bgoldbtbndlem2  46005  bgoldbtbndlem3  46006  lidldomn1  46226  cznnring  46261  rngccatidALTV  46294  ringccatidALTV  46357  scmsuppss  46455  lmodvsmdi  46465  gsumlsscl  46466  lindslinindimp2lem1  46546  lindsrng01  46556  elfzolborelfzop1  46607  difmodm1lt  46615  fllog2  46661  dignn0flhalflem1  46708  rrxlinesc  46828  itschlc0yqe  46853  itsclc0xyqsol  46861  itscnhlinecirc02p  46878
  Copyright terms: Public domain W3C validator