Theorem 3com12 1139

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3comr  1141  3com23  1142  brelrng  5932  fnunres2  6649  fresaunres1  6752  fvun2  6974  onfununi  8328  oaword  8534  nnaword  8613  nnmword  8619  naddel1  8674  naddss1  8676  ecopovtrn  8818  fpmg  8866  tskord  10765  ltadd2  11314  mul12  11375  add12  11428  addsub  11468  addsubeq4  11472  ppncan  11500  leadd1  11682  ltaddsub2  11689  leaddsub2  11691  ltsub1  11710  ltsub2  11711  div23  11891  ltmul1  12065  ltmulgt11  12074  lediv1  12080  lemuldiv  12095  ltdiv2  12101  zdiv  12666  xltadd1  13282  xltmul1  13318  iooneg  13498  icoshft  13500  fzaddel  13586  fzshftral  13643  modmulmodr  13973  facwordi  14325  pfxeq  14733  abssubge0  15379  climshftlem  15625  dvdsmul1  16335  divalglem8  16458  divalgb  16462  rprpwr  16617  lcmgcdeq  16670  pcfac  16959  mhmmulg  19181  rmodislmodlem  21028  xrsdsreval  21531  cnmptcom  23804  hmeof1o2  23889  ordthmeo  23928  isclmi0  25226  iscvsi  25257  cxplt2  26829  leadds1im  28146  ltadds2  28150  addscan2  28152  axcontlem8  29262  vcdi  30858  isvciOLD  30873  dipdi  31136  dipsubdi  31142  hvadd12  31328  hvmulcom  31336  his5  31379  bcs3  31476  chj12  31827  spansnmul  31857  homul12  32098  hoaddsub  32109  lnopmul  32260  lnopaddmuli  32266  lnopsubmuli  32268  lnfnaddmuli  32338  leop2  32417  dmdsl3  32608  chirredlem3  32685  atmd2  32693  cdj3lem3  32731  signstfvc  34906  3com12d  36711  cnambfre  38207  sdclem2  38281  indstrd  42850  addrcom  45075  uun123p1  45409  sineq0ALT  45537  stoweidlem17  46623  sigaras  47461  sigarms  47462  i0oii  49583