Theorem 3com12 1288

Description: Commutation in antecedent. Swap 1st and 2nd. (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 1062	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 207	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056

This theorem is referenced by:  3comr  1290  3com23  1291  3imp21  1298  3adant2l  1360  3adant2r  1361  brelrng  5387  fresaunres1  6115  fvun2  6309  onfununi  7483  oaword  7674  nnaword  7752  nnmword  7758  ecopovtrn  7893  fpmg  7925  tskord  9640  ltadd2  10179  mul12  10240  add12  10291  addsub  10330  addsubeq4  10334  ppncan  10361  leadd1  10534  ltaddsub2  10541  leaddsub2  10543  ltsub1  10562  ltsub2  10563  div23  10742  ltmul1  10911  ltmulgt11  10921  lediv1  10926  lemuldiv  10941  ltdiv2  10947  zdiv  11485  xltadd1  12124  xltmul1  12160  iooneg  12330  icoshft  12332  fzaddel  12413  fzshftral  12466  modmulmodr  12776  facwordi  13116  abssubge0  14111  climshftlem  14349  dvdsmul1  15050  divalglem8  15170  divalgb  15174  lcmgcdeq  15372  pcfac  15650  mhmmulg  17630  rmodislmodlem  18978  xrsdsreval  19839  cnmptcom  21529  hmeof1o2  21614  ordthmeo  21653  isclmi0  22944  iscvsi  22975  cxplt2  24489  axcontlem8  25896  2clwwlk2clwwlklem2lem2  27329  vcdi  27548  isvciOLD  27563  dipdi  27826  dipsubdi  27832  hvadd12  28020  hvmulcom  28028  his5  28071  bcs3  28168  chj12  28521  spansnmul  28551  homul12  28792  hoaddsub  28803  lnopmul  28954  lnopaddmuli  28960  lnopsubmuli  28962  lnfnaddmuli  29032  leop2  29111  dmdsl3  29302  chirredlem3  29379  atmd2  29387  cdj3lem3  29425  signstfvc  30779  3com12d  32429  cnambfre  33588  sdclem2  33668  addrcom  38996  uun123p1  39353  sineq0ALT  39487  stoweidlem17  40552  sigaras  41365  sigarms  41366