Theorem 3com12 1119

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3comr  1121  3com23  1122  brelrng  5813  fresaunres1  6553  fvun2  6757  onfununi  7980  oaword  8177  nnaword  8255  nnmword  8261  ecopovtrn  8402  fpmg  8434  tskord  10204  ltadd2  10746  mul12  10807  add12  10859  addsub  10899  addsubeq4  10903  ppncan  10930  leadd1  11110  ltaddsub2  11117  leaddsub2  11119  ltsub1  11138  ltsub2  11139  div23  11319  ltmul1  11492  ltmulgt11  11502  lediv1  11507  lemuldiv  11522  ltdiv2  11528  zdiv  12055  xltadd1  12652  xltmul1  12688  iooneg  12860  icoshft  12862  fzaddel  12944  fzshftral  12998  modmulmodr  13308  facwordi  13652  pfxeq  14060  abssubge0  14689  climshftlem  14933  dvdsmul1  15633  divalglem8  15753  divalgb  15757  lcmgcdeq  15958  pcfac  16237  mhmmulg  18270  rmodislmodlem  19703  xrsdsreval  20592  cnmptcom  22288  hmeof1o2  22373  ordthmeo  22412  isclmi0  23704  iscvsi  23735  cxplt2  25283  axcontlem8  26759  vcdi  28344  isvciOLD  28359  dipdi  28622  dipsubdi  28628  hvadd12  28814  hvmulcom  28822  his5  28865  bcs3  28962  chj12  29313  spansnmul  29343  homul12  29584  hoaddsub  29595  lnopmul  29746  lnopaddmuli  29752  lnopsubmuli  29754  lnfnaddmuli  29824  leop2  29903  dmdsl3  30094  chirredlem3  30171  atmd2  30179  cdj3lem3  30217  signstfvc  31846  3com12d  33660  cnambfre  34942  sdclem2  35019  addrcom  40814  uun123p1  41150  sineq0ALT  41278  stoweidlem17  42309  sigaras  43119  sigarms  43120