Theorem 3com12 1124

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3comr  1126  3com23  1127  brelrng  5952  fnunres2  6681  fresaunres1  6781  fvun2  7001  onfununi  8381  oaword  8587  nnaword  8665  nnmword  8671  naddel1  8725  naddss1  8727  ecopovtrn  8860  fpmg  8908  tskord  10820  ltadd2  11365  mul12  11426  add12  11479  addsub  11519  addsubeq4  11523  ppncan  11551  leadd1  11731  ltaddsub2  11738  leaddsub2  11740  ltsub1  11759  ltsub2  11760  div23  11941  ltmul1  12117  ltmulgt11  12127  lediv1  12133  lemuldiv  12148  ltdiv2  12154  zdiv  12688  xltadd1  13298  xltmul1  13334  iooneg  13511  icoshft  13513  fzaddel  13598  fzshftral  13655  modmulmodr  13978  facwordi  14328  pfxeq  14734  abssubge0  15366  climshftlem  15610  dvdsmul1  16315  divalglem8  16437  divalgb  16441  rprpwr  16596  lcmgcdeq  16649  pcfac  16937  mhmmulg  19133  rmodislmodlem  20927  xrsdsreval  21429  cnmptcom  23686  hmeof1o2  23771  ordthmeo  23810  isclmi0  25131  iscvsi  25162  cxplt2  26740  sleadd1im  28020  sltadd2  28024  addscan2  28026  axcontlem8  28986  vcdi  30584  isvciOLD  30599  dipdi  30862  dipsubdi  30868  hvadd12  31054  hvmulcom  31062  his5  31105  bcs3  31202  chj12  31553  spansnmul  31583  homul12  31824  hoaddsub  31835  lnopmul  31986  lnopaddmuli  31992  lnopsubmuli  31994  lnfnaddmuli  32064  leop2  32143  dmdsl3  32334  chirredlem3  32411  atmd2  32419  cdj3lem3  32457  signstfvc  34589  3com12d  36311  cnambfre  37675  sdclem2  37749  indstrd  42194  addrcom  44494  uun123p1  44829  sineq0ALT  44957  stoweidlem17  46032  sigaras  46870  sigarms  46871  i0oii  48817