Theorem 3com12 1209

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3adant2l  1234  3adant2r  1235  brelrng  4907  iotam  5260  funimaexglem  5351  fvun2  5640  nnaordi  6584  nnmword  6594  fpmg  6751  prcdnql  7579  prcunqu  7580  prarloc  7598  ltaprg  7714  mul12  8183  add12  8212  addsub  8265  addsubeq4  8269  ppncan  8296  leadd1  8485  ltaddsub2  8492  leaddsub2  8494  lemul1  8648  reapmul1lem  8649  reapadd1  8651  reapcotr  8653  remulext1  8654  div23ap  8746  ltmulgt11  8919  lediv1  8924  lemuldiv  8936  zdiv  9443  iooneg  10092  icoshft  10094  fzaddel  10163  fzshftral  10212  facwordi  10866  abssubge0  11332  climshftlemg  11532  dvdsmul1  12043  divalgb  12155  lcmgcdeq  12324  pcfac  12592  mhmmulg  13417  rmodislmodlem  14030  cnmptcom  14688  hmeof1o2  14698