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  6580  prcunqu  6581  prarloc  6599  ltaprg  6715  mul12  7140  add12  7167  addsub  7220  addsubeq4  7224  ppncan  7251  leadd1  7423  ltaddsub2  7430  leaddsub2  7432  lemul1  7582  reapmul1lem  7583  reapadd1  7585  reapcotr  7587  remulext1  7588  div23ap  7668  ltmulgt11  7828  lediv1  7833  lemuldiv  7845  zdiv  8326  iooneg  8854  icoshft  8856  fzaddel  8920  fzshftral  8968  abssubge0  9696  climshftlemg  9821
  Copyright terms: Public domain W3C validator