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

Theorem 3com12 1108
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 892 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜓𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbi 114 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  3adant2l  1129  3adant2r  1130  brelrng  4565  funimaexglem  4982  fvun2  5240  nnaordi  6081  nnmword  6091  prcdnql  6582  prcunqu  6583  prarloc  6601  ltaprg  6717  mul12  7142  add12  7169  addsub  7222  addsubeq4  7226  ppncan  7253  leadd1  7425  ltaddsub2  7432  leaddsub2  7434  lemul1  7584  reapmul1lem  7585  reapadd1  7587  reapcotr  7589  remulext1  7590  div23ap  7670  ltmulgt11  7830  lediv1  7835  lemuldiv  7847  zdiv  8328  iooneg  8856  icoshft  8858  fzaddel  8922  fzshftral  8970  abssubge0  9698  climshftlemg  9823
  Copyright terms: Public domain W3C validator