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

Theorem 3com12 1147
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 931 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜓𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbi 119 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 924
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 926
This theorem is referenced by:  3adant2l  1168  3adant2r  1169  brelrng  4666  funimaexglem  5097  fvun2  5371  nnaordi  6267  nnmword  6277  fpmg  6431  prcdnql  7043  prcunqu  7044  prarloc  7062  ltaprg  7178  mul12  7611  add12  7640  addsub  7693  addsubeq4  7697  ppncan  7724  leadd1  7908  ltaddsub2  7915  leaddsub2  7917  lemul1  8070  reapmul1lem  8071  reapadd1  8073  reapcotr  8075  remulext1  8076  div23ap  8158  ltmulgt11  8325  lediv1  8330  lemuldiv  8342  zdiv  8834  iooneg  9405  icoshft  9407  fzaddel  9473  fzshftral  9522  facwordi  10148  abssubge0  10535  climshftlemg  10690  dvdsmul1  11096  divalgb  11203  lcmgcdeq  11343
  Copyright terms: Public domain W3C validator