Theorem 3com12 1124

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3comr  1126  3com23  1127  brelrng  5896  fnunres2  6611  fresaunres1  6713  fvun2  6932  onfununi  8281  oaword  8484  nnaword  8563  nnmword  8569  naddel1  8623  naddss1  8625  ecopovtrn  8767  fpmg  8816  tskord  10703  ltadd2  11250  mul12  11311  add12  11364  addsub  11404  addsubeq4  11408  ppncan  11436  leadd1  11618  ltaddsub2  11625  leaddsub2  11627  ltsub1  11646  ltsub2  11647  div23  11828  ltmul1  12005  ltmulgt11  12015  lediv1  12021  lemuldiv  12036  ltdiv2  12042  zdiv  12599  xltadd1  13208  xltmul1  13244  iooneg  13424  icoshft  13426  fzaddel  13512  fzshftral  13569  modmulmodr  13899  facwordi  14251  pfxeq  14658  abssubge0  15290  climshftlem  15536  dvdsmul1  16246  divalglem8  16369  divalgb  16373  rprpwr  16528  lcmgcdeq  16581  pcfac  16870  mhmmulg  19091  rmodislmodlem  20924  xrsdsreval  21392  cnmptcom  23643  hmeof1o2  23728  ordthmeo  23767  isclmi0  25065  iscvsi  25096  cxplt2  26662  leadds1im  27979  ltadds2  27983  addscan2  27985  axcontlem8  29040  vcdi  30636  isvciOLD  30651  dipdi  30914  dipsubdi  30920  hvadd12  31106  hvmulcom  31114  his5  31157  bcs3  31254  chj12  31605  spansnmul  31635  homul12  31876  hoaddsub  31887  lnopmul  32038  lnopaddmuli  32044  lnopsubmuli  32046  lnfnaddmuli  32116  leop2  32195  dmdsl3  32386  chirredlem3  32463  atmd2  32471  cdj3lem3  32509  signstfvc  34718  3com12d  36492  cnambfre  37989  sdclem2  38063  indstrd  42632  addrcom  44901  uun123p1  45235  sineq0ALT  45363  stoweidlem17  46445  sigaras  47283  sigarms  47284  i0oii  49395