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  5890  fnunres2  6605  fresaunres1  6707  fvun2  6926  onfununi  8273  oaword  8476  nnaword  8555  nnmword  8561  naddel1  8615  naddss1  8617  ecopovtrn  8757  fpmg  8806  tskord  10691  ltadd2  11237  mul12  11298  add12  11351  addsub  11391  addsubeq4  11395  ppncan  11423  leadd1  11605  ltaddsub2  11612  leaddsub2  11614  ltsub1  11633  ltsub2  11634  div23  11815  ltmul1  11991  ltmulgt11  12001  lediv1  12007  lemuldiv  12022  ltdiv2  12028  zdiv  12562  xltadd1  13171  xltmul1  13207  iooneg  13387  icoshft  13389  fzaddel  13474  fzshftral  13531  modmulmodr  13860  facwordi  14212  pfxeq  14619  abssubge0  15251  climshftlem  15497  dvdsmul1  16204  divalglem8  16327  divalgb  16331  rprpwr  16486  lcmgcdeq  16539  pcfac  16827  mhmmulg  19045  rmodislmodlem  20880  xrsdsreval  21366  cnmptcom  23622  hmeof1o2  23707  ordthmeo  23746  isclmi0  25054  iscvsi  25085  cxplt2  26663  leadds1im  27983  ltadds2  27987  addscan2  27989  axcontlem8  29044  vcdi  30640  isvciOLD  30655  dipdi  30918  dipsubdi  30924  hvadd12  31110  hvmulcom  31118  his5  31161  bcs3  31258  chj12  31609  spansnmul  31639  homul12  31880  hoaddsub  31891  lnopmul  32042  lnopaddmuli  32048  lnopsubmuli  32050  lnfnaddmuli  32120  leop2  32199  dmdsl3  32390  chirredlem3  32467  atmd2  32475  cdj3lem3  32513  signstfvc  34731  3com12d  36504  cnambfre  37869  sdclem2  37943  indstrd  42447  addrcom  44715  uun123p1  45049  sineq0ALT  45177  stoweidlem17  46261  sigaras  47099  sigarms  47100  i0oii  49165