Theorem 3com12 1120

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3comr  1122  3com23  1123  brelrng  5949  fnunres2  6675  fresaunres1  6777  fvun2  6996  onfununi  8373  oaword  8581  nnaword  8659  nnmword  8665  naddel1  8719  naddss1  8721  ecopovtrn  8851  fpmg  8899  tskord  10825  ltadd2  11370  mul12  11431  add12  11483  addsub  11523  addsubeq4  11527  ppncan  11554  leadd1  11734  ltaddsub2  11741  leaddsub2  11743  ltsub1  11762  ltsub2  11763  div23  11944  ltmul1  12117  ltmulgt11  12127  lediv1  12133  lemuldiv  12148  ltdiv2  12154  zdiv  12686  xltadd1  13291  xltmul1  13327  iooneg  13504  icoshft  13506  fzaddel  13591  fzshftral  13645  modmulmodr  13959  facwordi  14308  pfxeq  14706  abssubge0  15334  climshftlem  15578  dvdsmul1  16282  divalglem8  16404  divalgb  16408  rprpwr  16562  lcmgcdeq  16615  pcfac  16903  mhmmulg  19111  rmodislmodlem  20907  xrsdsreval  21410  cnmptcom  23676  hmeof1o2  23761  ordthmeo  23800  isclmi0  25119  iscvsi  25150  cxplt2  26728  sleadd1im  28004  sltadd2  28008  addscan2  28010  axcontlem8  28908  vcdi  30501  isvciOLD  30516  dipdi  30779  dipsubdi  30785  hvadd12  30971  hvmulcom  30979  his5  31022  bcs3  31119  chj12  31470  spansnmul  31500  homul12  31741  hoaddsub  31752  lnopmul  31903  lnopaddmuli  31909  lnopsubmuli  31911  lnfnaddmuli  31981  leop2  32060  dmdsl3  32251  chirredlem3  32328  atmd2  32336  cdj3lem3  32374  signstfvc  34422  3com12d  36024  cnambfre  37371  sdclem2  37445  addrcom  44167  uun123p1  44503  sineq0ALT  44631  stoweidlem17  45656  sigaras  46494  sigarms  46495  i0oii  48271