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

Theorem 3com12 1143
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com12 ((𝜓𝜑𝜒) → 𝜃)

Proof of Theorem 3com12
StepHypRef Expression
1 3ancoma 927 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜓𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbi 119 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3adant2l  1164  3adant2r  1165  brelrng  4587  funimaexglem  5007  fvun2  5266  nnaordi  6140  nnmword  6150  prcdnql  6725  prcunqu  6726  prarloc  6744  ltaprg  6860  mul12  7293  add12  7322  addsub  7375  addsubeq4  7379  ppncan  7406  leadd1  7590  ltaddsub2  7597  leaddsub2  7599  lemul1  7749  reapmul1lem  7750  reapadd1  7752  reapcotr  7754  remulext1  7755  div23ap  7835  ltmulgt11  7998  lediv1  8003  lemuldiv  8015  zdiv  8505  iooneg  9075  icoshft  9077  fzaddel  9142  fzshftral  9190  facwordi  9753  abssubge0  10115  climshftlemg  10268  dvdsmul1  10351  divalgb  10458  lcmgcdeq  10598
  Copyright terms: Public domain W3C validator