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

Theorem com34 77
Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com4.1 (φ → (ψ → (χ → (θτ))))
Assertion
Ref Expression
com34 (φ → (ψ → (θ → (χτ))))

Proof of Theorem com34
StepHypRef Expression
1 com4.1 . 2 (φ → (ψ → (χ → (θτ))))
2 pm2.04 76 . 2 ((χ → (θτ)) → (θ → (χτ)))
31, 2syl6 29 1 (φ → (ψ → (θ → (χτ))))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  com4l  78  com35  84  3an1rs  1115  rspct  2643  po2nr  4037  funssres  4885  f1ocnv2d  5646  tfrlem9  5876  nnmass  6005  nnmordi  6025  genpcdl  6502  genpcuu  6503  mulnqprl  6549  mulnqpru  6550  distrlem1prl  6558  distrlem1pru  6559  divgt0  7619  divge0  7620  uzind2  8126
  Copyright terms: Public domain W3C validator