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

Theorem com34 83
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 82 . 2 ((𝜒 → (𝜃𝜏)) → (𝜃 → (𝜒𝜏)))
31, 2syl6 33 1 (𝜑 → (𝜓 → (𝜃 → (𝜒𝜏))))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com4l  84  com35  90  3an1rs  1219  rspct  2834  po2nr  4309  funssres  5258  f1ocnv2d  6074  tfrlem9  6319  nnmass  6487  nnmordi  6516  genpcdl  7517  genpcuu  7518  mulnqprl  7566  mulnqpru  7567  distrlem1prl  7580  distrlem1pru  7581  divgt0  8828  divge0  8829  uzind2  9364  facdiv  10717  dvdsabseq  11852  divgcdcoprm0  12100  lmodvsdi  13399
  Copyright terms: Public domain W3C validator