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  5887  fnunres2  6602  fresaunres1  6704  fvun2  6923  onfununi  8270  oaword  8473  nnaword  8551  nnmword  8557  naddel1  8611  naddss1  8613  ecopovtrn  8753  fpmg  8802  tskord  10682  ltadd2  11228  mul12  11289  add12  11342  addsub  11382  addsubeq4  11386  ppncan  11414  leadd1  11596  ltaddsub2  11603  leaddsub2  11605  ltsub1  11624  ltsub2  11625  div23  11806  ltmul1  11982  ltmulgt11  11992  lediv1  11998  lemuldiv  12013  ltdiv2  12019  zdiv  12553  xltadd1  13162  xltmul1  13198  iooneg  13378  icoshft  13380  fzaddel  13465  fzshftral  13522  modmulmodr  13851  facwordi  14203  pfxeq  14610  abssubge0  15242  climshftlem  15488  dvdsmul1  16195  divalglem8  16318  divalgb  16322  rprpwr  16477  lcmgcdeq  16530  pcfac  16818  mhmmulg  19036  rmodislmodlem  20871  xrsdsreval  21357  cnmptcom  23613  hmeof1o2  23698  ordthmeo  23737  isclmi0  25045  iscvsi  25076  cxplt2  26654  sleadd1im  27950  sltadd2  27954  addscan2  27956  axcontlem8  28970  vcdi  30566  isvciOLD  30581  dipdi  30844  dipsubdi  30850  hvadd12  31036  hvmulcom  31044  his5  31087  bcs3  31184  chj12  31535  spansnmul  31565  homul12  31806  hoaddsub  31817  lnopmul  31968  lnopaddmuli  31974  lnopsubmuli  31976  lnfnaddmuli  32046  leop2  32125  dmdsl3  32316  chirredlem3  32393  atmd2  32401  cdj3lem3  32439  signstfvc  34659  3com12d  36426  cnambfre  37781  sdclem2  37855  indstrd  42359  addrcom  44631  uun123p1  44965  sineq0ALT  45093  stoweidlem17  46177  sigaras  47015  sigarms  47016  i0oii  49081