Theorem 3com12 1141

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3comr  1143  3com23  1144  brelrng  5935  fnunres2  6682  fresaunres1  6785  fvun2  7008  onfununi  8387  oaword  8595  nnaword  8674  nnmword  8680  naddel1  8735  naddss1  8737  ecopovtrn  8879  fpmg  8934  tskord  10904  ltadd2  11453  mul12  11514  add12  11567  addsub  11607  addsubeq4  11611  ppncan  11639  leadd1  11824  ltaddsub2  11831  leaddsub2  11833  ltsub1  11852  ltsub2  11853  div23  12033  ltmul1  12207  ltmulgt11  12216  lediv1  12222  lemuldiv  12237  ltdiv2  12243  zdiv  12809  xltadd1  13426  xltmul1  13462  iooneg  13642  icoshft  13644  fzaddel  13732  fzshftral  13789  modmulmodr  14120  facwordi  14474  pfxeq  14887  abssubge0  15538  climshftlem  15785  dvdsmul1  16491  divalglem8  16614  divalgb  16618  rprpwr  16777  lcmgcdeq  16831  pcfac  17121  mhmmulg  19375  rmodislmodlem  21255  xrsdsreval  21770  cnmptcom  24052  hmeof1o2  24137  ordthmeo  24176  isclmi0  25474  iscvsi  25505  cxplt2  27083  leadds1im  28430  ltadds2  28434  addscan2  28436  axcontlem8  29606  vcdi  31224  isvciOLD  31239  dipdi  31502  dipsubdi  31508  hvadd12  31694  hvmulcom  31702  his5  31745  bcs3  31842  chj12  32193  spansnmul  32223  homul12  32464  hoaddsub  32475  lnopmul  32626  lnopaddmuli  32632  lnopsubmuli  32634  lnfnaddmuli  32704  leop2  32783  dmdsl3  32974  chirredlem3  33051  atmd2  33059  cdj3lem3  33097  signstfvc  35314  3com12d  37314  cnambfre  38854  sdclem2  38942  indstrd  43509  addrcom  45717  uun123p1  46051  sineq0ALT  46179  stoweidlem17  47300  sigaras  48138  sigarms  48139  i0oii  50365