New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3impa GIF version

Theorem 3impa 1146
 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
StepHypRef Expression
1 3impa.1 . . 3 (((φ ψ) χ) → θ)
21exp31 587 . 2 (φ → (ψ → (χθ)))
323imp 1145 1 ((φ ψ χ) → θ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934 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 177  df-an 360  df-3an 936 This theorem is referenced by:  3impdir  1238  syl3an9b  1250  biimp3a  1281  rspec3  2714  rspc3v  2964  raltpg  3777  rextpg  3778  eladdci  4399  lefinlteq  4463  opelopabt  4699  3optocl  4840  fun2ssres  5145  funssfv  5343  foco2  5426  f1elima  5474  eloprabga  5578  mucass  6135  cenc  6181
 Copyright terms: Public domain W3C validator