Theorem 3impa 1083

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 1082	1 ⊢ ((φ ∧ ψ ∧ χ) → θ)

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

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 873

This theorem is referenced by:  3impdir  1175  syl3an9b  1188  biimp3a  1218  rspec3  2383  rspc3v  2638  raltpg  3393  rextpg  3394  otexg  3937  opelopabt  3969  tpexg  4125  3optocl  4341  fun2ssres  4865  funssfv  5120  fvun1  5160  foco2  5239  f1elima  5333  eloprabga  5510  caovimo  5613  ot1stg  5698  ot2ndg  5699  ot3rdgg  5700  brtposg  5787  rdgexggg  5880  rdgivallem  5884  frecsuclem1  5899  nnmass  5977  nndir  5980  nnaword  5991  th3q  6118  ecovass  6122  ecoviass  6123  addasspig  6184  mulasspig  6186  mulcanpig  6189  ltapig  6192  ltmpig  6193  addassnqg  6235  ltbtwnnqq  6266  mulnnnq0  6299  addassnq0  6311  genpassl  6373  genpassu  6374  genpassg  6375  adddir  6614  addsub12  6811  subdir  6969