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  5905  fnunres2  6631  fresaunres1  6733  fvun2  6953  onfununi  8310  oaword  8513  nnaword  8591  nnmword  8597  naddel1  8651  naddss1  8653  ecopovtrn  8793  fpmg  8841  tskord  10733  ltadd2  11278  mul12  11339  add12  11392  addsub  11432  addsubeq4  11436  ppncan  11464  leadd1  11646  ltaddsub2  11653  leaddsub2  11655  ltsub1  11674  ltsub2  11675  div23  11856  ltmul1  12032  ltmulgt11  12042  lediv1  12048  lemuldiv  12063  ltdiv2  12069  zdiv  12604  xltadd1  13216  xltmul1  13252  iooneg  13432  icoshft  13434  fzaddel  13519  fzshftral  13576  modmulmodr  13902  facwordi  14254  pfxeq  14661  abssubge0  15294  climshftlem  15540  dvdsmul1  16247  divalglem8  16370  divalgb  16374  rprpwr  16529  lcmgcdeq  16582  pcfac  16870  mhmmulg  19047  rmodislmodlem  20835  xrsdsreval  21328  cnmptcom  23565  hmeof1o2  23650  ordthmeo  23689  isclmi0  24998  iscvsi  25029  cxplt2  26607  sleadd1im  27894  sltadd2  27898  addscan2  27900  axcontlem8  28898  vcdi  30494  isvciOLD  30509  dipdi  30772  dipsubdi  30778  hvadd12  30964  hvmulcom  30972  his5  31015  bcs3  31112  chj12  31463  spansnmul  31493  homul12  31734  hoaddsub  31745  lnopmul  31896  lnopaddmuli  31902  lnopsubmuli  31904  lnfnaddmuli  31974  leop2  32053  dmdsl3  32244  chirredlem3  32321  atmd2  32329  cdj3lem3  32367  signstfvc  34565  3com12d  36298  cnambfre  37662  sdclem2  37736  indstrd  42181  addrcom  44464  uun123p1  44798  sineq0ALT  44926  stoweidlem17  46015  sigaras  46853  sigarms  46854  i0oii  48908