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

Theorem 3com23 1110
 Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com23 ((𝜑𝜒𝜓) → 𝜃)

Proof of Theorem 3com23
StepHypRef Expression
1 3exp.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213exp 1103 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 72 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
433imp 1098 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:  3coml  1111  syld3an2  1182  3anidm13  1193  eqreu  2733  f1ofveu  5500  acexmid  5511  dfsmo2  5902  f1oeng  6237  ltexprlemdisj  6704  ltexprlemfu  6709  recexprlemss1u  6734  mul32  7143  add32  7170  cnegexlem2  7187  subsub23  7216  subadd23  7223  addsub12  7224  subsub  7241  subsub3  7243  sub32  7245  suble  7435  lesub  7436  ltsub23  7437  ltsub13  7438  ltleadd  7441  div32ap  7671  div13ap  7672  div12ap  7673  divdiv32ap  7696  cju  7913  icc0r  8795  fzen  8907  elfz1b  8952  elfzmlbmOLD  8989  expival  9257  expgt0  9288  expge0  9291  expge1  9292  shftval2  9427  abs3dif  9701
 Copyright terms: Public domain W3C validator