Theorem 3impa 1098

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 346	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	3imp 1097	1 ⊢ ((φ ∧ ψ ∧ χ) → θ)

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  3impdir  1190  syl3an9b  1204  biimp3a  1234  stoic3  1317  rspec3  2403  rspc3v  2659  raltpg  3414  rextpg  3415  otexg  3958  opelopabt  3990  tpexg  4145  3optocl  4361  fun2ssres  4886  funssfv  5142  fvun1  5182  foco2  5261  f1elima  5355  eloprabga  5533  caovimo  5636  ot1stg  5721  ot2ndg  5722  ot3rdgg  5723  brtposg  5810  rdgexggg  5904  rdgivallem  5908  frecsuclem1  5926  nnmass  6005  nndir  6008  nnaword  6020  th3q  6147  ecovass  6151  ecoviass  6152  addasspig  6314  mulasspig  6316  mulcanpig  6319  ltapig  6322  ltmpig  6323  addassnqg  6366  ltbtwnnqq  6398  mulnnnq0  6433  addassnq0  6445  genpassl  6507  genpassu  6508  genpassg  6509  aptiprleml  6611  adddir  6816  le2tri3i  6923  addsub12  7021  subdir  7179  reapmul1  7379  recexaplem2  7415  div12ap  7455  divdiv32ap  7478  divdivap1  7481  zaddcllemneg  8060  fnn0ind  8130  xrltso  8487  iccgelb  8571  elicc4  8579  elfz  8650  fzrevral  8737  expivallem  8910  expnegap0  8917  expgt0  8942  expge0  8945  expge1  8946  mulexpzap  8949  expp1zap  8957  expm1ap  8958