ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3com23 Structured version   GIF version

Theorem 3com23 1094
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3com23 ((φ χ ψ) → θ)

Proof of Theorem 3com23
StepHypRef Expression
1 3exp.1 . . . 4 ((φ ψ χ) → θ)
213exp 1087 . . 3 (φ → (ψ → (χθ)))
32com23 72 . 2 (φ → (χ → (ψθ)))
433imp 1082 1 ((φ χ ψ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   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:  3coml  1095  syld3an2  1166  3anidm13  1177  eqreu  2706  f1ofveu  5420  acexmid  5431  dfsmo2  5820  ltexprlemdisj  6437  ltexprlemfu  6442  recexprlemss1u  6464  mul32  6730  add32  6757  cnegexlem2  6774  subsub23  6803  subadd23  6810  addsub12  6811  subsub  6827  subsub3  6829  sub32  6831  suble  7020  lesub  7021  ltsub23  7022  ltsub13  7023  ltleadd  7026
  Copyright terms: Public domain W3C validator