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  4988  iotam  5344  funimaexglem  5439  fresaunres1disj  5546  fvun2  5744  nnaordi  6741  nnmword  6751  fpmg  6908  prcdnql  7799  prcunqu  7800  prarloc  7818  ltaprg  7934  mul12  8402  add12  8431  addsub  8484  addsubeq4  8488  ppncan  8515  leadd1  8704  ltaddsub2  8711  leaddsub2  8713  lemul1  8867  reapmul1lem  8868  reapadd1  8870  reapcotr  8872  remulext1  8873  div23ap  8965  ltmulgt11  9138  lediv1  9143  lemuldiv  9155  zdiv  9666  iooneg  10321  icoshft  10323  fzaddel  10393  fzshftral  10442  facwordi  11102  pfxeq  11388  abssubge0  11787  climshftlemg  11987  dvdsmul1  12499  divalgb  12611  lcmgcdeq  12780  pcfac  13048  mhmmulg  13880  rmodislmodlem  14498  cnmptcom  15163  hmeof1o2  15173