Theorem 3impa 1278

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3impa.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3impa	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 629	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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:  ex3  1282  3impdir  1422  syl3an9b  1437  biimp3a  1472  stoic3  1741  rspec3  2964  rspc3v  3356  raltpg  4268  rextpg  4269  disjiun  4672  otthg  4983  3optocl  5231  fun2ssres  5969  funtpg  5980  funssfv  6247  foco2OLD  6420  f1elima  6560  ot1stg  7224  ot2ndg  7225  smogt  7509  omord2  7692  omword  7695  oeword  7715  omabslem  7771  ecovass  7897  fpmg  7925  findcard  8240  cdaun  9032  cfsmolem  9130  ingru  9675  addasspi  9755  mulasspi  9757  ltapi  9763  ltmpi  9764  axpre-ltadd  10026  leltne  10165  dedekind  10238  recextlem2  10696  divdiv32  10771  divdiv1  10774  lble  11013  fnn0ind  11514  supminf  11813  xrleltne  12016  xrmaxeq  12048  xrmineq  12049  iccgelb  12268  elicc4  12278  iccsplit  12343  elfz  12370  fzrevral  12463  modabs  12743  expgt0  12933  expge0  12936  expge1  12937  mulexpz  12940  expp1z  12949  expm1  12950  digit1  13038  faclbnd4  13124  faclbnd5  13125  s3eqs2s1eq  13729  abssubne0  14100  binom  14606  dvds0lem  15039  dvdsnegb  15046  muldvds1  15053  muldvds2  15054  dvdscmulr  15057  dvdsmulcr  15058  divalgmodcl  15178  gcd2n0cl  15278  gcdaddm  15293  lcmdvds  15368  prmdvdsexp  15474  rpexp1i  15480  monpropd  16444  prfval  16886  xpcpropd  16895  curf2ndf  16934  eqglact  17692  mndodcongi  18008  oddvdsnn0  18009  efgi0  18179  efgi1  18180  lss0cl  18995  scmatscmid  20360  pmatcollpw3fi1lem1  20639  cnpval  21088  cnf2  21101  cnnei  21134  lfinun  21376  ptpjcn  21462  cnmptk2  21537  flfval  21841  cnmpt2plusg  21939  cnmpt2vsca  22045  ustincl  22058  xbln0  22266  blssec  22287  blpnfctr  22288  mopni2  22345  mopni3  22346  nmoval  22566  nmocl  22571  isnghm2  22575  isnmhm2  22603  cnmpt2ds  22693  metdseq0  22704  cnmpt2ip  23093  caucfil  23127  mbfimasn  23446  dvnf  23735  dvnbss  23736  coemul  24053  dvply1  24084  dvnply2  24087  pserdvlem2  24227  logeftb  24375  advlogexp  24446  cxpne0  24468  cxpp1  24471  lgsne0  25105  f1otrg  25796  ax5seglem9  25862  uhgrn0  26007  upgrn0  26029  upgrle  26030  uhgrwkspthlem2  26706  frgrhash2wsp  27312  sspval  27706  sspnval  27720  lnof  27738  nmooval  27746  nmooge0  27750  nmoub3i  27756  bloln  27767  nmblore  27769  hosval  28727  homval  28728  hodval  28729  hfsval  28730  hfmval  28731  homulass  28789  hoadddir  28791  nmopub2tALT  28896  nmfnleub2  28913  kbval  28941  lnopmul  28954  0lnfn  28972  lnopcoi  28990  nmcoplb  29017  nmcfnlb  29041  kbass2  29104  nmopleid  29126  hstoh  29219  mdi  29282  dmdi  29289  dmdi4  29294  supxrnemnf  29662  reofld  29968  bnj605  31103  bnj607  31112  bnj1097  31175  elno2  31932  topdifinffinlem  33325  lindsdom  33533  lindsenlbs  33534  ftc1anclem2  33616  fzmul  33667  nninfnub  33677  exidreslem  33806  grposnOLD  33811  ghomf  33819  rngohomf  33895  rngohom1  33897  rngohomadd  33898  rngohommul  33899  rngoiso1o  33908  rngoisohom  33909  igenmin  33993  lkrcl  34697  lkrf0  34698  omlfh1N  34863  tendoex  36580  3anrabdioph  37663  3orrabdioph  37664  rencldnfilem  37701  expmordi  37829  dvdsabsmod0  37871  jm2.18  37872  jm2.25  37883  jm2.15nn0  37887  addrfv  38990  subrfv  38991  mulvfv  38992  bi3impa  39007  ssfiunibd  39837  supminfxr  40007  limsupgtlem  40327  xlimmnfv  40378  xlimpnfv  40382  dvnmul  40476  stoweidlem34  40569  stoweidlem48  40583  sge0cl  40916  sge0xp  40964  ovnsubaddlem1  41105  ovnovollem3  41193  aovmpt4g  41602  gboge9  41977