Theorem 3com12 1141

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3comr  1143  3com23  1144  brelrng  5933  fnunres2  6652  fresaunres1  6755  fvun2  6977  onfununi  8330  oaword  8536  nnaword  8615  nnmword  8621  naddel1  8676  naddss1  8678  ecopovtrn  8820  fpmg  8868  tskord  10776  ltadd2  11325  mul12  11386  add12  11439  addsub  11479  addsubeq4  11483  ppncan  11511  leadd1  11693  ltaddsub2  11700  leaddsub2  11702  ltsub1  11721  ltsub2  11722  div23  11902  ltmul1  12076  ltmulgt11  12085  lediv1  12091  lemuldiv  12106  ltdiv2  12112  zdiv  12677  xltadd1  13293  xltmul1  13329  iooneg  13509  icoshft  13511  fzaddel  13598  fzshftral  13655  modmulmodr  13986  facwordi  14338  pfxeq  14750  abssubge0  15398  climshftlem  15644  dvdsmul1  16352  divalglem8  16475  divalgb  16479  rprpwr  16634  lcmgcdeq  16687  pcfac  16976  mhmmulg  19204  rmodislmodlem  21079  xrsdsreval  21591  cnmptcom  23864  hmeof1o2  23949  ordthmeo  23988  isclmi0  25286  iscvsi  25317  cxplt2  26892  leadds1im  28209  ltadds2  28213  addscan2  28215  axcontlem8  29350  vcdi  30946  isvciOLD  30961  dipdi  31224  dipsubdi  31230  hvadd12  31416  hvmulcom  31424  his5  31467  bcs3  31564  chj12  31915  spansnmul  31945  homul12  32186  hoaddsub  32197  lnopmul  32348  lnopaddmuli  32354  lnopsubmuli  32356  lnfnaddmuli  32426  leop2  32505  dmdsl3  32696  chirredlem3  32773  atmd2  32781  cdj3lem3  32819  signstfvc  34985  3com12d  36855  cnambfre  38352  sdclem2  38426  indstrd  42993  addrcom  45216  uun123p1  45550  sineq0ALT  45678  stoweidlem17  46764  sigaras  47602  sigarms  47603  i0oii  49731