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

Theorem 3imp 1275
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 1056 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 447 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3sylbi 207 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  3imp31  1276  3imp231  1277  3impa  1278  3impb  1279  3impia  1280  3impib  1281  3com23OLD  1293  3imp21  1298  3an1rsOLD  1301  3imp1  1302  3impd  1303  syl3an2  1400  syl3an3  1401  3jao  1429  biimp3ar  1473  3elpr2eq  4467  wefrc  5137  predpo  5736  f1ssf1  6206  fveqdmss  6394  poxp  7334  fvn0elsuppb  7357  smo11  7506  odi  7704  omass  7705  nndi  7748  nnmass  7749  undifixp  7986  isinf  8214  domunfican  8274  infssuni  8298  pr2nelem  8865  dfac8alem  8890  fin33i  9229  fin1a2lem10  9269  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  axdc4lem  9315  ttukeyg  9377  axdclem  9379  grupr  9657  nqereu  9789  squeeze0  10964  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  xnn0lenn0nn0  12113  supxrun  12184  difelfzle  12491  elfzo0z  12549  fzofzim  12554  fzo1fzo0n0  12558  elfzodifsumelfzo  12573  elfznelfzo  12613  injresinj  12629  mulexp  12939  expadd  12942  expmul  12945  bernneq  13030  facdiv  13114  hashgt12el2  13249  hashimarni  13266  leisorel  13282  fi1uzind  13317  2swrd1eqwrdeq  13500  swrdswrdlem  13505  swrdccat3  13538  swrdccatid  13543  repswswrd  13577  cshf1  13602  2cshwcshw  13617  cshimadifsn  13621  swrdco  13629  relexpindlem  13847  dvdsaddre2b  15076  addmodlteqALT  15094  ltoddhalfle  15132  halfleoddlt  15133  dfgcd2  15310  coprmprod  15422  coprmproddvds  15424  cncongr1  15428  oddprmgt2  15458  prmfac1  15478  infpnlem1  15661  prmgaplem5  15806  prmgaplem6  15807  cshwshashlem1  15849  setsstruct  15945  iscatd2  16389  initoeu2lem2  16712  clatleglb  17173  dfgrp3e  17562  mulgaddcom  17611  mulginvcom  17612  symgfvne  17854  f1rhm0to0ALT  18789  lmodvsmmulgdi  18946  lsmcv  19189  assamulgscm  19398  psrvscafval  19438  mamufacex  20243  mat1scmat  20393  gsummatr01lem4  20512  cramer0  20544  chpscmat  20695  fvmptnn04ifa  20703  fvmptnn04ifc  20705  fvmptnn04ifd  20706  fiinopn  20754  opnneissb  20966  cnpimaex  21108  regsep  21186  hausnei2  21205  cmpsublem  21250  cmpsub  21251  filufint  21771  blssps  22276  blss  22277  mblsplit  23346  bcmono  25047  gausslemma2dlem1a  25135  2sqlem10  25198  upgrex  26032  numedglnl  26084  ausgrumgri  26107  ausgrusgri  26108  usgredg2vtxeuALT  26159  ushgredgedg  26166  ushgredgedgloop  26168  edg0usgr  26190  0uhgrsubgr  26216  subumgredg2  26222  fusgrfisbase  26265  cusgrsizeinds  26404  cusgrsize2inds  26405  finsumvtxdg2size  26502  upgrewlkle2  26558  wlkl1loop  26590  pthdivtx  26681  2pthnloop  26683  upgrwlkdvde  26689  uhgrwkspthlem2  26706  usgr2pthlem  26715  usgr2pth  26716  clwlkl1loop  26734  crctcshwlkn0lem4  26761  wwlksnextproplem3  26874  wspn0  26889  umgr2adedgwlkonALT  26912  umgr2wlk  26914  umgr2wlkon  26915  elwwlks2  26933  umgrclwwlkge2  26957  clwlkclwwlklem2  26966  clwwlknlbonbgr1  27002  clwwlkn1loopb  27006  clwwlkel  27009  clwwlkext2edg  27020  clwwlknonex2lem2  27083  clwwlknonex2  27084  clwwlknonex2e  27085  1pthon2v  27131  uhgr3cyclex  27160  eupth2lem3lem6  27211  frgr3vlem1  27253  3cyclfrgrrn1  27265  frgrnbnb  27273  frgrwopreglem4a  27290  2clwwlk2clwwlklem2  27330  clwwlkccatlem  27331  extwwlkfab  27342  frgrregord013  27382  frgrregord13  27383  frgrogt3nreg  27384  friendship  27386  chcompl  28227  spansncol  28555  hoaddsub  28803  bnj600  31115  sconnpht  31337  msubvrs  31583  funpsstri  31789  imp5p  32430  cntotbnd  33725  clmgmOLD  33780  grpomndo  33804  rngoneglmul  33872  rngonegrmul  33873  zerdivemp1x  33876  atlex  34921  cvlexch1  34933  cvlsupr4  34950  cvlsupr5  34951  cvlsupr6  34952  2llnneN  35013  athgt  35060  llnle  35122  lplnle  35144  lvoli2  35185  pmaple  35365  dalawlem10  35484  dalawlem13  35487  dalawlem14  35488  dalaw  35490  lhp2lt  35605  ldilval  35717  cdleme50trn2  36156  cdlemf  36168  cdlemg18b  36284  tendotp  36366  tendospcanN  36629  dihmeetlem3N  36911  dvh4dimlem  37049  pell14qrexpclnn0  37747  pell1qrgap  37755  aomclem2  37942  rngunsnply  38060  relexpxpmin  38326  relexpaddss  38327  rp-simp2  38404  gneispaceel2  38759  bi33imp12  39013  bi23imp13  39014  bi13imp23  39015  bi23imp1  39018  bi123imp0  39019  ee333  39030  jaoded  39099  e333  39277  suctrALTcf  39472  suctrALTcfVD  39473  ax6e2ndeqALT  39481  mullimc  40166  mullimcf  40173  fzopredsuc  41658  subsubelfzo0  41661  iccpartimp  41678  iccpartigtl  41684  lswn0  41705  pfxfv  41724  pfxccat3  41751  reuccatpfxs1lem  41758  fmtnofac1  41807  pwdif  41826  lighneallem2  41848  lighneallem3  41849  lighneallem4  41852  mogoldbblem  41954  gbegt5  41974  sbgoldbaltlem1  41992  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  lidldomn1  42246  cznnring  42281  rngccatidALTV  42314  ringccatidALTV  42377  scmsuppss  42478  lmodvsmdi  42488  gsumlsscl  42489  lindslinindimp2lem1  42572  lindsrng01  42582  elfzolborelfzop1  42634  difmodm1lt  42642  fllog2  42687  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator