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

Theorem 3imp 1108
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 421 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1107 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3imp31  1109  3imp231  1110  3impb  1112  3impib  1113  3imp1  1344  3impd  1345  3jao  1422  biimp3ar  1467  3elpr2eq  4802  wefrc  5517  predpo  6138  iotan0  6318  f1ssf1  6625  fveqdmss  6827  funelss  7732  poxp  7809  fvn0elsuppb  7834  suppfnss  7842  smo11  7988  odi  8192  omass  8193  nndi  8236  nnmass  8237  undifixp  8485  domunfican  8779  preleqg  9066  pr2nelem  9419  dfac8alem  9444  fin33i  9784  domtriomlem  9857  axdc3lem2  9866  axdc3lem4  9868  axdc4lem  9870  ttukeyg  9932  axdclem  9934  grupr  10212  nqereu  10344  squeeze0  11536  rpnnen1lem5  12372  xnn0lenn0nn0  12630  supxrun  12701  difelfzle  13019  elfzo0z  13078  fzofzim  13083  fzo1fzo0n0  13087  elfzodifsumelfzo  13102  elfznelfzo  13141  injresinj  13157  mulexp  13468  expadd  13471  expmul  13474  facdiv  13647  hashgt12el2  13784  hashimarni  13802  leisorel  13818  fi1uzind  13855  pfxfv  14039  swrdswrdlem  14061  pfxccat3  14091  reuccatpfxs1lem  14103  repswswrd  14141  cshf1  14167  2cshwcshw  14182  cshimadifsn  14186  relexpindlem  14417  pwdif  15218  dvdsaddre2b  15652  addmodlteqALT  15670  ltoddhalfle  15705  halfleoddlt  15706  coprmprod  15998  coprmproddvds  16000  cncongr1  16004  oddprmgt2  16036  prmfac1  16056  infpnlem1  16239  prmgaplem5  16384  prmgaplem6  16385  cshwshashlem1  16424  setsstruct  16518  iscatd2  16947  initoeu2lem2  17270  clatleglb  17731  dfgrp3e  18194  mulgaddcom  18246  mulginvcom  18247  symgfvne  18504  f1rhm0to0ALT  19492  lsmcv  19909  assamulgscm  20590  psrvscafval  20631  mat1scmat  21147  cramer0  21298  chpscmat  21450  fvmptnn04ifa  21458  fvmptnn04ifc  21460  fvmptnn04ifd  21461  fiinopn  21509  opnneissb  21722  cnpimaex  21864  regsep  21942  hausnei2  21961  cmpsublem  22007  cmpsub  22008  filufint  22528  blssps  23034  blss  23035  mblsplit  24139  bcmono  25864  gausslemma2dlem1a  25952  2sqlem10  26015  elntg2  26782  upgrex  26888  numedglnl  26940  ausgrumgri  26963  ausgrusgri  26964  usgredg2vtxeuALT  27015  ushgredgedg  27022  ushgredgedgloop  27024  edg0usgr  27046  0uhgrsubgr  27072  subumgredg2  27078  fusgrfisbase  27121  cusgrsizeinds  27245  cusgrsize2inds  27246  finsumvtxdg2size  27343  upgrewlkle2  27399  wlkl1loop  27430  pthdivtx  27521  2pthnloop  27523  upgrwlkdvde  27529  uhgrwkspthlem2  27546  usgr2pthlem  27555  usgr2pth  27556  clwlkl1loop  27575  crctcshwlkn0lem4  27602  wwlksnextproplem3  27700  wspn0  27713  umgr2adedgwlkonALT  27736  umgr2wlk  27738  umgr2wlkon  27739  elwwlks2  27755  clwwlkccatlem  27777  umgrclwwlkge2  27779  clwlkclwwlklem2  27788  clwlkclwwlkf1lem2  27793  clwlkclwwlkf  27796  clwwlknlbonbgr1  27827  clwwlkn1loopb  27831  clwwlkel  27834  clwwlkext2edg  27844  clwwlknonex2lem2  27896  clwwlknonex2  27897  clwwlknonex2e  27898  1pthon2v  27941  uhgr3cyclex  27970  eupth2lem3lem6  28021  frgr3vlem1  28061  3cyclfrgrrn1  28073  frgrnbnb  28081  frgrwopreglem4a  28098  2clwwlk2clwwlklem  28134  wlkl0  28155  frgrregord013  28183  frgrregord13  28184  frgrogt3nreg  28185  friendship  28187  chcompl  29028  spansncol  29354  hoaddsub  29602  bnj600  32299  sconnpht  32584  satffunlem  32756  satfvel  32767  msubvrs  32915  funpsstri  33116  imp5p  33767  cntotbnd  35227  clmgmOLD  35282  grpomndo  35306  rngoneglmul  35374  rngonegrmul  35375  zerdivemp1x  35378  atlex  36605  cvlexch1  36617  cvlsupr4  36634  cvlsupr5  36635  cvlsupr6  36636  2llnneN  36698  athgt  36745  llnle  36807  lplnle  36829  lvoli2  36870  pmaple  37050  dalawlem10  37169  dalawlem13  37172  dalawlem14  37173  dalaw  37175  lhp2lt  37290  ldilval  37402  cdleme50trn2  37840  cdlemf  37852  cdlemg18b  37968  tendotp  38050  tendospcanN  38312  dihmeetlem3N  38594  dvh4dimlem  38732  pell14qrexpclnn0  39794  pell1qrgap  39802  aomclem2  39986  rngunsnply  40104  relexpaddss  40406  rp-simp2  40481  gneispaceel2  40834  bi33imp12  41183  bi23imp13  41184  bi13imp23  41185  bi23imp1  41188  bi123imp0  41189  ee333  41200  jaoded  41259  e333  41426  suctrALTcf  41615  suctrALTcfVD  41616  ax6e2ndeqALT  41624  mullimc  42245  mullimcf  42252  f1oresf1o2  43834  fzopredsuc  43867  subsubelfzo0  43870  elsetpreimafvbi  43895  iccpartimp  43921  iccpartigtl  43927  lswn0  43948  poprelb  44028  fmtnofac1  44074  lighneallem2  44111  lighneallem3  44112  lighneallem4  44115  mogoldbblem  44225  fpprel2  44246  gbegt5  44266  sbgoldbaltlem1  44284  bgoldbtbndlem2  44311  bgoldbtbndlem3  44312  lidldomn1  44532  cznnring  44567  rngccatidALTV  44600  ringccatidALTV  44663  scmsuppss  44761  lmodvsmdi  44771  gsumlsscl  44772  lindslinindimp2lem1  44854  lindsrng01  44864  elfzolborelfzop1  44915  difmodm1lt  44923  fllog2  44969  dignn0flhalflem1  45016  rrxlinesc  45136  itschlc0yqe  45161  itsclc0xyqsol  45169  itscnhlinecirc02p  45186
  Copyright terms: Public domain W3C validator