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  5883  fnunres2  6595  fresaunres1  6697  fvun2  6915  onfununi  8264  oaword  8467  nnaword  8545  nnmword  8551  naddel1  8605  naddss1  8607  ecopovtrn  8747  fpmg  8795  tskord  10674  ltadd2  11220  mul12  11281  add12  11334  addsub  11374  addsubeq4  11378  ppncan  11406  leadd1  11588  ltaddsub2  11595  leaddsub2  11597  ltsub1  11616  ltsub2  11617  div23  11798  ltmul1  11974  ltmulgt11  11984  lediv1  11990  lemuldiv  12005  ltdiv2  12011  zdiv  12546  xltadd1  13158  xltmul1  13194  iooneg  13374  icoshft  13376  fzaddel  13461  fzshftral  13518  modmulmodr  13844  facwordi  14196  pfxeq  14602  abssubge0  15235  climshftlem  15481  dvdsmul1  16188  divalglem8  16311  divalgb  16315  rprpwr  16470  lcmgcdeq  16523  pcfac  16811  mhmmulg  18994  rmodislmodlem  20832  xrsdsreval  21318  cnmptcom  23563  hmeof1o2  23648  ordthmeo  23687  isclmi0  24996  iscvsi  25027  cxplt2  26605  sleadd1im  27899  sltadd2  27903  addscan2  27905  axcontlem8  28916  vcdi  30509  isvciOLD  30524  dipdi  30787  dipsubdi  30793  hvadd12  30979  hvmulcom  30987  his5  31030  bcs3  31127  chj12  31478  spansnmul  31508  homul12  31749  hoaddsub  31760  lnopmul  31911  lnopaddmuli  31917  lnopsubmuli  31919  lnfnaddmuli  31989  leop2  32068  dmdsl3  32259  chirredlem3  32336  atmd2  32344  cdj3lem3  32382  signstfvc  34542  3com12d  36288  cnambfre  37652  sdclem2  37726  indstrd  42170  addrcom  44452  uun123p1  44786  sineq0ALT  44914  stoweidlem17  46002  sigaras  46840  sigarms  46841  i0oii  48908