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 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  1125  3com23  1126  brelrng  5966  fnunres2  6692  fresaunres1  6794  fvun2  7014  onfununi  8397  oaword  8605  nnaword  8683  nnmword  8689  naddel1  8743  naddss1  8745  ecopovtrn  8878  fpmg  8926  tskord  10849  ltadd2  11394  mul12  11455  add12  11507  addsub  11547  addsubeq4  11551  ppncan  11578  leadd1  11758  ltaddsub2  11765  leaddsub2  11767  ltsub1  11786  ltsub2  11787  div23  11968  ltmul1  12144  ltmulgt11  12154  lediv1  12160  lemuldiv  12175  ltdiv2  12181  zdiv  12713  xltadd1  13318  xltmul1  13354  iooneg  13531  icoshft  13533  fzaddel  13618  fzshftral  13672  modmulmodr  13988  facwordi  14338  pfxeq  14744  abssubge0  15376  climshftlem  15620  dvdsmul1  16326  divalglem8  16448  divalgb  16452  rprpwr  16606  lcmgcdeq  16659  pcfac  16946  mhmmulg  19155  rmodislmodlem  20949  xrsdsreval  21452  cnmptcom  23707  hmeof1o2  23792  ordthmeo  23831  isclmi0  25150  iscvsi  25181  cxplt2  26758  sleadd1im  28038  sltadd2  28042  addscan2  28044  axcontlem8  29004  vcdi  30597  isvciOLD  30612  dipdi  30875  dipsubdi  30881  hvadd12  31067  hvmulcom  31075  his5  31118  bcs3  31215  chj12  31566  spansnmul  31596  homul12  31837  hoaddsub  31848  lnopmul  31999  lnopaddmuli  32005  lnopsubmuli  32007  lnfnaddmuli  32077  leop2  32156  dmdsl3  32347  chirredlem3  32424  atmd2  32432  cdj3lem3  32470  signstfvc  34551  3com12d  36276  cnambfre  37628  sdclem2  37702  indstrd  42150  addrcom  44444  uun123p1  44780  sineq0ALT  44908  stoweidlem17  45938  sigaras  46776  sigarms  46777  i0oii  48599