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

Theorem 3com12 1185
 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 969 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜓𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbi 120 1 ((𝜓𝜑𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 964 This theorem is referenced by:  3adant2l  1210  3adant2r  1211  brelrng  4765  funimaexglem  5201  fvun2  5481  nnaordi  6397  nnmword  6407  fpmg  6561  prcdnql  7285  prcunqu  7286  prarloc  7304  ltaprg  7420  mul12  7884  add12  7913  addsub  7966  addsubeq4  7970  ppncan  7997  leadd1  8185  ltaddsub2  8192  leaddsub2  8194  lemul1  8348  reapmul1lem  8349  reapadd1  8351  reapcotr  8353  remulext1  8354  div23ap  8444  ltmulgt11  8615  lediv1  8620  lemuldiv  8632  zdiv  9132  iooneg  9764  icoshft  9766  fzaddel  9832  fzshftral  9881  facwordi  10479  abssubge0  10867  climshftlemg  11064  dvdsmul1  11504  divalgb  11611  lcmgcdeq  11753  cnmptcom  12456  hmeof1o2  12466
 Copyright terms: Public domain W3C validator