Theorem 3com12 1234

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 1012	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 121	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3adant2l  1259  3adant2r  1260  brelrng  4969  iotam  5325  funimaexglem  5420  fvun2  5722  nnaordi  6719  nnmword  6729  fpmg  6886  prcdnql  7747  prcunqu  7748  prarloc  7766  ltaprg  7882  mul12  8350  add12  8379  addsub  8432  addsubeq4  8436  ppncan  8463  leadd1  8652  ltaddsub2  8659  leaddsub2  8661  lemul1  8815  reapmul1lem  8816  reapadd1  8818  reapcotr  8820  remulext1  8821  div23ap  8913  ltmulgt11  9086  lediv1  9091  lemuldiv  9103  zdiv  9612  iooneg  10267  icoshft  10269  fzaddel  10339  fzshftral  10388  facwordi  11048  pfxeq  11326  abssubge0  11725  climshftlemg  11925  dvdsmul1  12437  divalgb  12549  lcmgcdeq  12718  pcfac  12986  mhmmulg  13813  rmodislmodlem  14429  cnmptcom  15092  hmeof1o2  15102