Theorem 3impa 1196

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 364	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1195	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  ex3  1197  3impdir  1306  syl3an9b  1322  biimp3a  1357  stoic3  1450  rspec3  2595  rspc3v  2892  raltpg  3685  rextpg  3686  disjiun  4038  otexg  4273  opelopabt  4307  tpexg  4490  3optocl  4752  fun2ssres  5313  funssfv  5601  fvun1  5644  foco2  5821  f1elima  5841  eloprabga  6031  caovimo  6139  ot1stg  6237  ot2ndg  6238  ot3rdgg  6239  brtposg  6339  rdgexggg  6462  rdgivallem  6466  nnmass  6572  nndir  6575  nnaword  6596  th3q  6726  ecovass  6730  ecoviass  6731  fpmg  6760  findcard  6984  unfiin  7022  addasspig  7442  mulasspig  7444  mulcanpig  7447  ltapig  7450  ltmpig  7451  addassnqg  7494  ltbtwnnqq  7527  mulnnnq0  7562  addassnq0  7574  genpassl  7636  genpassu  7637  genpassg  7638  aptiprleml  7751  adddir  8062  le2tri3i  8180  addsub12  8284  subdir  8457  reapmul1  8667  recexaplem2  8724  div12ap  8766  divdiv32ap  8792  divdivap1  8795  lble  9019  zaddcllemneg  9410  fnn0ind  9488  xrltso  9917  iccgelb  10053  elicc4  10061  elfz  10135  fzrevral  10226  expnegap0  10690  expgt0  10715  expge0  10718  expge1  10719  mulexpzap  10722  expp1zap  10731  expm1ap  10732  apexp1  10861  ccatsymb  11056  abssubap0  11372  binom  11766  dvds0lem  12083  dvdsnegb  12090  muldvds1  12098  muldvds2  12099  divalgmodcl  12210  gcd2n0cl  12261  lcmdvds  12372  prmdvdsexp  12441  rpexp1i  12447  eqglact  13532  lss0cl  14102  cnpval  14641  cnf2  14648  cnnei  14675  blssec  14881  blpnfctr  14882  mopni2  14926  mopni3  14927  dvply1  15208