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  1221  rspct  2849  po2nr  4330  funssres  5280  f1ocnv2d  6102  tfrlem9  6348  nnmass  6516  nnmordi  6545  genpcdl  7553  genpcuu  7554  mulnqprl  7602  mulnqpru  7603  distrlem1prl  7616  distrlem1pru  7617  divgt0  8864  divge0  8865  uzind2  9400  facdiv  10759  dvdsabseq  11894  divgcdcoprm0  12144  lmodvsdi  13652
  Copyright terms: Public domain W3C validator