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

Theorem 3com23 1109
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 1102 . . 3 (φ → (ψ → (χθ)))
32com23 72 . 2 (φ → (χ → (ψθ)))
433imp 1097 1 ((φ χ ψ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   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:  3coml  1110  syld3an2  1181  3anidm13  1192  eqreu  2727  f1ofveu  5443  acexmid  5454  dfsmo2  5843  f1oeng  6173  ltexprlemdisj  6579  ltexprlemfu  6584  recexprlemss1u  6607  mul32  6920  add32  6947  cnegexlem2  6964  subsub23  6993  subadd23  7000  addsub12  7001  subsub  7017  subsub3  7019  sub32  7021  suble  7210  lesub  7211  ltsub23  7212  ltsub13  7213  ltleadd  7216  div32ap  7433  div13ap  7434  div12ap  7435  divdiv32ap  7458  cju  7674  icc0r  8545  fzen  8657  elfz1b  8702  elfzmlbmOLD  8739  expival  8891  expgt0  8922  expge0  8925  expge1  8926
  Copyright terms: Public domain W3C validator