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

Theorem com34 81
 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 80 . 2 ((𝜒 → (𝜃𝜏)) → (𝜃 → (𝜒𝜏)))
31, 2syl6 33 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  82  com35  88  3an1rs  1127  rspct  2666  po2nr  4074  funssres  4970  f1ocnv2d  5732  tfrlem9  5966  nnmass  6097  nnmordi  6120  genpcdl  6675  genpcuu  6676  mulnqprl  6724  mulnqpru  6725  distrlem1prl  6738  distrlem1pru  6739  divgt0  7913  divge0  7914  uzind2  8409  facdiv  9606  dvdsabseq  10159
 Copyright terms: Public domain W3C validator