Theorem 3com12 1231

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  3adant2l  1256  3adant2r  1257  brelrng  4954  iotam  5309  funimaexglem  5403  fvun2  5700  nnaordi  6652  nnmword  6662  fpmg  6819  prcdnql  7667  prcunqu  7668  prarloc  7686  ltaprg  7802  mul12  8271  add12  8300  addsub  8353  addsubeq4  8357  ppncan  8384  leadd1  8573  ltaddsub2  8580  leaddsub2  8582  lemul1  8736  reapmul1lem  8737  reapadd1  8739  reapcotr  8741  remulext1  8742  div23ap  8834  ltmulgt11  9007  lediv1  9012  lemuldiv  9024  zdiv  9531  iooneg  10180  icoshft  10182  fzaddel  10251  fzshftral  10300  facwordi  10957  pfxeq  11223  abssubge0  11608  climshftlemg  11808  dvdsmul1  12319  divalgb  12431  lcmgcdeq  12600  pcfac  12868  mhmmulg  13695  rmodislmodlem  14308  cnmptcom  14966  hmeof1o2  14976