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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  com4l  84  com35  90  3an1rs  1165  rspct  2737  po2nr  4169  funssres  5101  f1ocnv2d  5906  tfrlem9  6146  nnmass  6313  nnmordi  6342  genpcdl  7228  genpcuu  7229  mulnqprl  7277  mulnqpru  7278  distrlem1prl  7291  distrlem1pru  7292  divgt0  8488  divge0  8489  uzind2  9015  facdiv  10325  dvdsabseq  11340  divgcdcoprm0  11575
  Copyright terms: Public domain W3C validator