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 1115	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3comr  1126  3com23  1127  brelrng  5941  fnunres2  6663  fresaunres1  6765  fvun2  6984  onfununi  8341  oaword  8549  nnaword  8627  nnmword  8633  naddel1  8686  naddss1  8688  ecopovtrn  8814  fpmg  8862  tskord  10775  ltadd2  11318  mul12  11379  add12  11431  addsub  11471  addsubeq4  11475  ppncan  11502  leadd1  11682  ltaddsub2  11689  leaddsub2  11691  ltsub1  11710  ltsub2  11711  div23  11891  ltmul1  12064  ltmulgt11  12074  lediv1  12079  lemuldiv  12094  ltdiv2  12100  zdiv  12632  xltadd1  13235  xltmul1  13271  iooneg  13448  icoshft  13450  fzaddel  13535  fzshftral  13589  modmulmodr  13902  facwordi  14249  pfxeq  14646  abssubge0  15274  climshftlem  15518  dvdsmul1  16221  divalglem8  16343  divalgb  16347  rprpwr  16500  lcmgcdeq  16549  pcfac  16832  mhmmulg  18995  rmodislmodlem  20539  xrsdsreval  20990  cnmptcom  23182  hmeof1o2  23267  ordthmeo  23306  isclmi0  24614  iscvsi  24645  cxplt2  26206  sleadd1im  27473  sltadd2  27477  addscan2  27479  axcontlem8  28260  vcdi  29849  isvciOLD  29864  dipdi  30127  dipsubdi  30133  hvadd12  30319  hvmulcom  30327  his5  30370  bcs3  30467  chj12  30818  spansnmul  30848  homul12  31089  hoaddsub  31100  lnopmul  31251  lnopaddmuli  31257  lnopsubmuli  31259  lnfnaddmuli  31329  leop2  31408  dmdsl3  31599  chirredlem3  31676  atmd2  31684  cdj3lem3  31722  signstfvc  33616  3com12d  35243  cnambfre  36584  sdclem2  36658  addrcom  43282  uun123p1  43618  sineq0ALT  43746  stoweidlem17  44781  sigaras  45619  sigarms  45620  i0oii  47600