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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3comr  1126  3com23  1127  brelrng  5890  fnunres2  6605  fresaunres1  6707  fvun2  6926  onfununi  8274  oaword  8477  nnaword  8556  nnmword  8562  naddel1  8616  naddss1  8618  ecopovtrn  8760  fpmg  8809  tskord  10694  ltadd2  11241  mul12  11302  add12  11355  addsub  11395  addsubeq4  11399  ppncan  11427  leadd1  11609  ltaddsub2  11616  leaddsub2  11618  ltsub1  11637  ltsub2  11638  div23  11819  ltmul1  11996  ltmulgt11  12006  lediv1  12012  lemuldiv  12027  ltdiv2  12033  zdiv  12590  xltadd1  13199  xltmul1  13235  iooneg  13415  icoshft  13417  fzaddel  13503  fzshftral  13560  modmulmodr  13890  facwordi  14242  pfxeq  14649  abssubge0  15281  climshftlem  15527  dvdsmul1  16237  divalglem8  16360  divalgb  16364  rprpwr  16519  lcmgcdeq  16572  pcfac  16861  mhmmulg  19082  rmodislmodlem  20915  xrsdsreval  21401  cnmptcom  23653  hmeof1o2  23738  ordthmeo  23777  isclmi0  25075  iscvsi  25106  cxplt2  26675  leadds1im  27993  ltadds2  27997  addscan2  27999  axcontlem8  29054  vcdi  30651  isvciOLD  30666  dipdi  30929  dipsubdi  30935  hvadd12  31121  hvmulcom  31129  his5  31172  bcs3  31269  chj12  31620  spansnmul  31650  homul12  31891  hoaddsub  31902  lnopmul  32053  lnopaddmuli  32059  lnopsubmuli  32061  lnfnaddmuli  32131  leop2  32210  dmdsl3  32401  chirredlem3  32478  atmd2  32486  cdj3lem3  32524  signstfvc  34734  3com12d  36508  cnambfre  38003  sdclem2  38077  indstrd  42646  addrcom  44919  uun123p1  45253  sineq0ALT  45381  stoweidlem17  46463  sigaras  47301  sigarms  47302  i0oii  49407