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  6432  addassnq0  6444  genpassl  6506  genpassu  6507  genpassg  6508  aptiprleml  6610  adddir  6796  le2tri3i  6903  addsub12  7001  subdir  7159  reapmul1  7359  recexaplem2  7395  div12ap  7435  divdiv32ap  7458  divdivap1  7461  zaddcllemneg  8040  fnn0ind  8110  xrltso  8467  iccgelb  8551  elicc4  8559  elfz  8630  fzrevral  8717  expivallem  8890  expnegap0  8897  expgt0  8922  expge0  8925  expge1  8926  mulexpzap  8929  expp1zap  8937  expm1ap  8938