Theorem 3com12 1135

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 1131	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp21 1125	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3comr  1137  3com23  1138  brelrng  5913  fnunres2  6629  fresaunres1  6732  fvun2  6954  onfununi  8306  oaword  8512  nnaword  8591  nnmword  8597  naddel1  8652  naddss1  8654  ecopovtrn  8796  fpmg  8844  tskord  10732  ltadd2  11281  mul12  11342  add12  11395  addsub  11435  addsubeq4  11439  ppncan  11467  leadd1  11649  ltaddsub2  11656  leaddsub2  11658  ltsub1  11677  ltsub2  11678  div23  11858  ltmul1  12035  ltmulgt11  12045  lediv1  12051  lemuldiv  12066  ltdiv2  12072  zdiv  12637  xltadd1  13253  xltmul1  13289  iooneg  13469  icoshft  13471  fzaddel  13557  fzshftral  13614  modmulmodr  13944  facwordi  14296  pfxeq  14703  abssubge0  15346  climshftlem  15592  dvdsmul1  16302  divalglem8  16425  divalgb  16429  rprpwr  16584  lcmgcdeq  16637  pcfac  16926  mhmmulg  19148  rmodislmodlem  20984  xrsdsreval  21452  cnmptcom  23726  hmeof1o2  23811  ordthmeo  23850  isclmi0  25148  iscvsi  25179  cxplt2  26751  leadds1im  28068  ltadds2  28072  addscan2  28074  axcontlem8  29129  vcdi  30725  isvciOLD  30740  dipdi  31003  dipsubdi  31009  hvadd12  31195  hvmulcom  31203  his5  31246  bcs3  31343  chj12  31694  spansnmul  31724  homul12  31965  hoaddsub  31976  lnopmul  32127  lnopaddmuli  32133  lnopsubmuli  32135  lnfnaddmuli  32205  leop2  32284  dmdsl3  32475  chirredlem3  32552  atmd2  32560  cdj3lem3  32598  signstfvc  34829  3com12d  36631  cnambfre  38128  sdclem2  38202  indstrd  42771  addrcom  45011  uun123p1  45345  sineq0ALT  45473  stoweidlem17  46552  sigaras  47390  sigarms  47391  i0oii  49502