Theorem impcom 125

Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
imp.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
impcom	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 30	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 124	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  mpan9  281  19.41h  1709  19.41  1710  equtr2  1735  mopick  2133  2euex  2142  gencl  2806  2gencl  2807  vtocl4g  2846  vtocl4ga  2847  rspccva  2880  indifdir  3433  sseq0  3506  minel  3526  r19.2m  3551  r19.2mOLD  3552  elelpwi  3633  ssuni  3878  disjiun  4046  trintssm  4166  ssexg  4191  pofun  4367  sowlin  4375  2optocl  4760  3optocl  4761  ssrelrn  4878  elrnmpt1  4938  resieq  4978  fnun  5391  fss  5447  fun  5459  dmfex  5477  fvelimab  5648  mptfvex  5678  fmptco  5759  fnressn  5783  fressnfv  5784  fvtp2g  5806  fvtp3g  5807  fnex  5819  funfvima3  5831  isores3  5897  f1o2ndf1  6327  reldmtpos  6352  smores  6391  tfrlem7  6416  tfrlemi1  6431  tfrexlem  6433  tfrcl  6463  frecrdg  6507  nnacl  6579  nnmcl  6580  nnmsucr  6587  nntri3or  6592  nnaword  6610  nnaordex  6627  2ecoptocl  6723  ssct  6928  enm  6930  xpf1o  6956  ac6sfi  7010  f1dmvrnfibi  7061  f1vrnfibi  7062  updjud  7199  enumct  7232  nnnninfeq  7245  exmidontriimlem4  7352  exmidontriim  7353  elni2  7447  ax1rid  8010  negf1o  8474  mulgt1  8956  lbreu  9038  nnaddcl  9076  nnmulcl  9077  zaddcllempos  9429  zaddcllemneg  9431  nn0n0n1ge2b  9472  fzind  9508  fnn0ind  9509  uzaddcl  9727  elpq  9790  uzsubsubfz  10189  elfz1b  10232  elfz0ubfz0  10267  fz0fzdiffz0  10272  elfzmlbp  10274  fzofzim  10334  elfzom1elp1fzo  10353  elfzom1p1elfzo  10365  ssfzo12bi  10376  modfzo0difsn  10562  seq3val  10627  seqvalcd  10628  expcllem  10717  expap0  10736  apexp1  10885  faclbnd  10908  faclbnd6  10911  fihashf1rn  10955  omgadd  10969  hashfzp1  10991  seq3coll  11009  fundm2domnop0  11012  lswlgt0cl  11068  ccatsymb  11081  swrdnd  11135  swrd0g  11136  swrdspsleq  11143  pfxsuff1eqwrdeq  11175  swrdswrdlem  11180  swrdswrd  11181  wrd2ind  11199  cjexp  11279  r19.29uz  11378  resqrexlemover  11396  resqrexlemlo  11399  resqrexlemcalc3  11402  absexp  11465  fimaxre2  11613  climshft  11690  climub  11730  climserle  11731  sumfct  11760  isumss2  11779  binom  11870  bcxmas  11875  clim2prod  11925  prodfap0  11931  prodfrecap  11932  prodfct  11973  demoivreALT  12160  dvdsdivcl  12236  dvdsfac  12246  oddnn02np1  12266  oddge22np1  12267  evennn02n  12268  evennn2n  12269  m1exp1  12287  nn0o  12293  flodddiv4  12322  gcdneg  12378  bezoutlemmain  12394  dfgcd2  12410  gcdmultiple  12416  nnwosdc  12435  alginv  12444  cncongr1  12500  prmdvdsexp  12545  prmndvdsfaclt  12553  dfgrp2  13434  srgmulgass  13826  lmodvsmmulgdi  14160  lmodfopnelem1  14161  rmodislmodlem  14187  cnfldmulg  14413  cnfldexp  14414  clsss  14665  xmettri2  14908  mettri  14920  metss  15041  plycolemc  15305  zabsle1  15551  gausslemma2dlem1a  15610  gausslemma2dlem2  15614  gausslemma2dlem3  15615  gausslemma2dlem4  15616  2lgslem1a1  15638  incistruhgr  15761  bdssexg  15978  bj-findis  16053  nninfalllem1  16086  nninfsellemdc  16088  redc0  16137