Theorem 3com12 1141

Description: Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com12	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem 3com12

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1137	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp21 1131	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3comr  1143  3com23  1144  brelrng  5933  fnunres2  6650  fresaunres1  6753  fvun2  6975  onfununi  8329  oaword  8535  nnaword  8614  nnmword  8620  naddel1  8675  naddss1  8677  ecopovtrn  8819  fpmg  8867  tskord  10766  ltadd2  11315  mul12  11376  add12  11429  addsub  11469  addsubeq4  11473  ppncan  11501  leadd1  11683  ltaddsub2  11690  leaddsub2  11692  ltsub1  11711  ltsub2  11712  div23  11892  ltmul1  12066  ltmulgt11  12075  lediv1  12081  lemuldiv  12096  ltdiv2  12102  zdiv  12667  xltadd1  13283  xltmul1  13319  iooneg  13499  icoshft  13501  fzaddel  13588  fzshftral  13645  modmulmodr  13975  facwordi  14327  pfxeq  14735  abssubge0  15381  climshftlem  15627  dvdsmul1  16336  divalglem8  16459  divalgb  16463  rprpwr  16618  lcmgcdeq  16671  pcfac  16960  mhmmulg  19182  rmodislmodlem  21031  xrsdsreval  21543  cnmptcom  23816  hmeof1o2  23901  ordthmeo  23940  isclmi0  25238  iscvsi  25269  cxplt2  26844  leadds1im  28161  ltadds2  28165  addscan2  28167  axcontlem8  29302  vcdi  30898  isvciOLD  30913  dipdi  31176  dipsubdi  31182  hvadd12  31368  hvmulcom  31376  his5  31419  bcs3  31516  chj12  31867  spansnmul  31897  homul12  32138  hoaddsub  32149  lnopmul  32300  lnopaddmuli  32306  lnopsubmuli  32308  lnfnaddmuli  32378  leop2  32457  dmdsl3  32648  chirredlem3  32725  atmd2  32733  cdj3lem3  32771  signstfvc  34942  3com12d  36803  cnambfre  38300  sdclem2  38374  indstrd  42941  addrcom  45166  uun123p1  45500  sineq0ALT  45628  stoweidlem17  46714  sigaras  47552  sigarms  47553  i0oii  49681