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  2835  po2nr  4310  funssres  5259  f1ocnv2d  6075  tfrlem9  6320  nnmass  6488  nnmordi  6517  genpcdl  7518  genpcuu  7519  mulnqprl  7567  mulnqpru  7568  distrlem1prl  7581  distrlem1pru  7582  divgt0  8829  divge0  8830  uzind2  9365  facdiv  10718  dvdsabseq  11853  divgcdcoprm0  12101  lmodvsdi  13401
  Copyright terms: Public domain W3C validator