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

Theorem com34 82
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 81 . 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  83  com35  89  3an1rs  1153  rspct  2708  po2nr  4109  funssres  5018  f1ocnv2d  5799  tfrlem9  6032  nnmass  6196  nnmordi  6221  genpcdl  7015  genpcuu  7016  mulnqprl  7064  mulnqpru  7065  distrlem1prl  7078  distrlem1pru  7079  divgt0  8261  divge0  8262  uzind2  8784  facdiv  10035  dvdsabseq  10715  divgcdcoprm0  10950
  Copyright terms: Public domain W3C validator