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

Step	Hyp	Ref	Expression
1		3ancoma 892	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 114	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

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