Theorem 3com12 1210

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  3adant2l  1235  3adant2r  1236  brelrng  4918  iotam  5272  funimaexglem  5366  fvun2  5659  nnaordi  6607  nnmword  6617  fpmg  6774  prcdnql  7617  prcunqu  7618  prarloc  7636  ltaprg  7752  mul12  8221  add12  8250  addsub  8303  addsubeq4  8307  ppncan  8334  leadd1  8523  ltaddsub2  8530  leaddsub2  8532  lemul1  8686  reapmul1lem  8687  reapadd1  8689  reapcotr  8691  remulext1  8692  div23ap  8784  ltmulgt11  8957  lediv1  8962  lemuldiv  8974  zdiv  9481  iooneg  10130  icoshft  10132  fzaddel  10201  fzshftral  10250  facwordi  10907  pfxeq  11172  abssubge0  11488  climshftlemg  11688  dvdsmul1  12199  divalgb  12311  lcmgcdeq  12480  pcfac  12748  mhmmulg  13574  rmodislmodlem  14187  cnmptcom  14845  hmeof1o2  14855