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  6599  fresaunres1  6701  fvun2  6919  onfununi  8271  oaword  8474  nnaword  8552  nnmword  8558  naddel1  8612  naddss1  8614  ecopovtrn  8754  fpmg  8802  tskord  10693  ltadd2  11238  mul12  11299  add12  11352  addsub  11392  addsubeq4  11396  ppncan  11424  leadd1  11606  ltaddsub2  11613  leaddsub2  11615  ltsub1  11634  ltsub2  11635  div23  11816  ltmul1  11992  ltmulgt11  12002  lediv1  12008  lemuldiv  12023  ltdiv2  12029  zdiv  12564  xltadd1  13176  xltmul1  13212  iooneg  13392  icoshft  13394  fzaddel  13479  fzshftral  13536  modmulmodr  13862  facwordi  14214  pfxeq  14620  abssubge0  15253  climshftlem  15499  dvdsmul1  16206  divalglem8  16329  divalgb  16333  rprpwr  16488  lcmgcdeq  16541  pcfac  16829  mhmmulg  19012  rmodislmodlem  20850  xrsdsreval  21336  cnmptcom  23581  hmeof1o2  23666  ordthmeo  23705  isclmi0  25014  iscvsi  25045  cxplt2  26623  sleadd1im  27917  sltadd2  27921  addscan2  27923  axcontlem8  28934  vcdi  30527  isvciOLD  30542  dipdi  30805  dipsubdi  30811  hvadd12  30997  hvmulcom  31005  his5  31048  bcs3  31145  chj12  31496  spansnmul  31526  homul12  31767  hoaddsub  31778  lnopmul  31929  lnopaddmuli  31935  lnopsubmuli  31937  lnfnaddmuli  32007  leop2  32086  dmdsl3  32277  chirredlem3  32354  atmd2  32362  cdj3lem3  32400  signstfvc  34544  3com12d  36286  cnambfre  37650  sdclem2  37724  indstrd  42169  addrcom  44451  uun123p1  44785  sineq0ALT  44913  stoweidlem17  46002  sigaras  46840  sigarms  46841  i0oii  48908