Theorem 3com12 1123

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3comr  1125  3com23  1126  brelrng  5921  fnunres2  6651  fresaunres1  6751  fvun2  6971  onfununi  8355  oaword  8561  nnaword  8639  nnmword  8645  naddel1  8699  naddss1  8701  ecopovtrn  8834  fpmg  8882  tskord  10794  ltadd2  11339  mul12  11400  add12  11453  addsub  11493  addsubeq4  11497  ppncan  11525  leadd1  11705  ltaddsub2  11712  leaddsub2  11714  ltsub1  11733  ltsub2  11734  div23  11915  ltmul1  12091  ltmulgt11  12101  lediv1  12107  lemuldiv  12122  ltdiv2  12128  zdiv  12663  xltadd1  13272  xltmul1  13308  iooneg  13488  icoshft  13490  fzaddel  13575  fzshftral  13632  modmulmodr  13955  facwordi  14307  pfxeq  14714  abssubge0  15346  climshftlem  15590  dvdsmul1  16297  divalglem8  16419  divalgb  16423  rprpwr  16578  lcmgcdeq  16631  pcfac  16919  mhmmulg  19098  rmodislmodlem  20886  xrsdsreval  21379  cnmptcom  23616  hmeof1o2  23701  ordthmeo  23740  isclmi0  25049  iscvsi  25080  cxplt2  26659  sleadd1im  27946  sltadd2  27950  addscan2  27952  axcontlem8  28950  vcdi  30546  isvciOLD  30561  dipdi  30824  dipsubdi  30830  hvadd12  31016  hvmulcom  31024  his5  31067  bcs3  31164  chj12  31515  spansnmul  31545  homul12  31786  hoaddsub  31797  lnopmul  31948  lnopaddmuli  31954  lnopsubmuli  31956  lnfnaddmuli  32026  leop2  32105  dmdsl3  32296  chirredlem3  32373  atmd2  32381  cdj3lem3  32419  signstfvc  34606  3com12d  36328  cnambfre  37692  sdclem2  37766  indstrd  42206  addrcom  44499  uun123p1  44833  sineq0ALT  44961  stoweidlem17  46046  sigaras  46884  sigarms  46885  i0oii  48894