Theorem 3com12 1233

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  3adant2l  1258  3adant2r  1259  brelrng  4963  iotam  5318  funimaexglem  5413  fvun2  5713  nnaordi  6675  nnmword  6685  fpmg  6842  prcdnql  7703  prcunqu  7704  prarloc  7722  ltaprg  7838  mul12  8307  add12  8336  addsub  8389  addsubeq4  8393  ppncan  8420  leadd1  8609  ltaddsub2  8616  leaddsub2  8618  lemul1  8772  reapmul1lem  8773  reapadd1  8775  reapcotr  8777  remulext1  8778  div23ap  8870  ltmulgt11  9043  lediv1  9048  lemuldiv  9060  zdiv  9567  iooneg  10222  icoshft  10224  fzaddel  10293  fzshftral  10342  facwordi  11001  pfxeq  11276  abssubge0  11662  climshftlemg  11862  dvdsmul1  12373  divalgb  12485  lcmgcdeq  12654  pcfac  12922  mhmmulg  13749  rmodislmodlem  14363  cnmptcom  15021  hmeof1o2  15031