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

Theorem 3imp 1103
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 418 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1102 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3imp31  1104  3imp231  1105  3impb  1107  3impib  1108  3imp1  1339  3impd  1340  3jao  1417  biimp3ar  1461  3elpr2eq  4831  wefrc  5543  predpo  6160  iotan0  6339  f1ssf1  6640  fveqdmss  6839  funelss  7737  poxp  7813  fvn0elsuppb  7838  suppfnss  7846  smo11  7992  odi  8195  omass  8196  nndi  8239  nnmass  8240  undifixp  8487  domunfican  8780  preleqg  9067  pr2nelem  9419  dfac8alem  9444  fin33i  9780  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  ttukeyg  9928  axdclem  9930  grupr  10208  nqereu  10340  squeeze0  11532  rpnnen1lem5  12370  xnn0lenn0nn0  12628  supxrun  12699  difelfzle  13010  elfzo0z  13069  fzofzim  13074  fzo1fzo0n0  13078  elfzodifsumelfzo  13093  elfznelfzo  13132  injresinj  13148  mulexp  13458  expadd  13461  expmul  13464  facdiv  13637  hashgt12el2  13774  hashimarni  13792  leisorel  13808  fi1uzind  13845  pfxfv  14034  swrdswrdlem  14056  pfxccat3  14086  reuccatpfxs1lem  14098  repswswrd  14136  cshf1  14162  2cshwcshw  14177  cshimadifsn  14181  relexpindlem  14412  pwdif  15213  dvdsaddre2b  15647  addmodlteqALT  15665  ltoddhalfle  15700  halfleoddlt  15701  coprmprod  15995  coprmproddvds  15997  cncongr1  16001  oddprmgt2  16033  prmfac1  16053  infpnlem1  16236  prmgaplem5  16381  prmgaplem6  16382  cshwshashlem1  16419  setsstruct  16513  iscatd2  16942  initoeu2lem2  17265  clatleglb  17726  dfgrp3e  18139  mulgaddcom  18191  mulginvcom  18192  symgfvne  18446  f1rhm0to0ALT  19425  lsmcv  19844  assamulgscm  20060  psrvscafval  20100  mat1scmat  21078  cramer0  21229  chpscmat  21380  fvmptnn04ifa  21388  fvmptnn04ifc  21390  fvmptnn04ifd  21391  fiinopn  21439  opnneissb  21652  cnpimaex  21794  regsep  21872  hausnei2  21891  cmpsublem  21937  cmpsub  21938  filufint  22458  blssps  22963  blss  22964  mblsplit  24062  bcmono  25781  gausslemma2dlem1a  25869  2sqlem10  25932  elntg2  26699  upgrex  26805  numedglnl  26857  ausgrumgri  26880  ausgrusgri  26881  usgredg2vtxeuALT  26932  ushgredgedg  26939  ushgredgedgloop  26941  edg0usgr  26963  0uhgrsubgr  26989  subumgredg2  26995  fusgrfisbase  27038  cusgrsizeinds  27162  cusgrsize2inds  27163  finsumvtxdg2size  27260  upgrewlkle2  27316  wlkl1loop  27347  pthdivtx  27438  2pthnloop  27440  upgrwlkdvde  27446  uhgrwkspthlem2  27463  usgr2pthlem  27472  usgr2pth  27473  clwlkl1loop  27492  crctcshwlkn0lem4  27519  wwlksnextproplem3  27618  wspn0  27631  umgr2adedgwlkonALT  27654  umgr2wlk  27656  umgr2wlkon  27657  elwwlks2  27673  clwwlkccatlem  27695  umgrclwwlkge2  27697  clwlkclwwlklem2  27706  clwlkclwwlkf1lem2  27711  clwlkclwwlkf  27714  clwwlknlbonbgr1  27745  clwwlkn1loopb  27749  clwwlkel  27753  clwwlkext2edg  27763  clwwlknonex2lem2  27815  clwwlknonex2  27816  clwwlknonex2e  27817  1pthon2v  27860  uhgr3cyclex  27889  eupth2lem3lem6  27940  frgr3vlem1  27980  3cyclfrgrrn1  27992  frgrnbnb  28000  frgrwopreglem4a  28017  2clwwlk2clwwlklem  28053  wlkl0  28074  frgrregord013  28102  frgrregord13  28103  frgrogt3nreg  28104  friendship  28106  chcompl  28947  spansncol  29273  hoaddsub  29521  bnj600  32091  sconnpht  32374  satffunlem  32546  satfvel  32557  msubvrs  32705  funpsstri  32906  imp5p  33557  cntotbnd  34957  clmgmOLD  35012  grpomndo  35036  rngoneglmul  35104  rngonegrmul  35105  zerdivemp1x  35108  atlex  36334  cvlexch1  36346  cvlsupr4  36363  cvlsupr5  36364  cvlsupr6  36365  2llnneN  36427  athgt  36474  llnle  36536  lplnle  36558  lvoli2  36599  pmaple  36779  dalawlem10  36898  dalawlem13  36901  dalawlem14  36902  dalaw  36904  lhp2lt  37019  ldilval  37131  cdleme50trn2  37569  cdlemf  37581  cdlemg18b  37697  tendotp  37779  tendospcanN  38041  dihmeetlem3N  38323  dvh4dimlem  38461  pell14qrexpclnn0  39343  pell1qrgap  39351  aomclem2  39535  rngunsnply  39653  relexpaddss  39943  rp-simp2  40019  gneispaceel2  40374  bi33imp12  40704  bi23imp13  40705  bi13imp23  40706  bi23imp1  40709  bi123imp0  40710  ee333  40721  jaoded  40780  e333  40947  suctrALTcf  41136  suctrALTcfVD  41137  ax6e2ndeqALT  41145  mullimc  41777  mullimcf  41784  f1oresf1o2  43371  fzopredsuc  43404  subsubelfzo0  43407  iccpartimp  43424  iccpartigtl  43430  lswn0  43451  poprelb  43533  fmtnofac1  43579  lighneallem2  43618  lighneallem3  43619  lighneallem4  43622  mogoldbblem  43732  fpprel2  43753  gbegt5  43773  sbgoldbaltlem1  43791  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  lidldomn1  44090  cznnring  44125  rngccatidALTV  44158  ringccatidALTV  44221  scmsuppss  44318  lmodvsmdi  44328  gsumlsscl  44329  lindslinindimp2lem1  44411  lindsrng01  44421  elfzolborelfzop1  44472  difmodm1lt  44480  fllog2  44526  dignn0flhalflem1  44573  rrxlinesc  44620  itschlc0yqe  44645  itsclc0xyqsol  44653  itscnhlinecirc02p  44670
  Copyright terms: Public domain W3C validator