Theorem impcom 124

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 123	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpan9  279  19.41h  1663  19.41  1664  equtr2  1687  mopick  2077  2euex  2086  gencl  2718  2gencl  2719  rspccva  2788  indifdir  3332  sseq0  3404  minel  3424  r19.2m  3449  r19.2mOLD  3450  elelpwi  3522  ssuni  3758  disjiun  3924  trintssm  4042  ssexg  4067  pofun  4234  sowlin  4242  2optocl  4616  3optocl  4617  elrnmpt1  4790  resieq  4829  fnun  5229  fss  5284  fun  5295  dmfex  5312  fvelimab  5477  mptfvex  5506  fmptco  5586  fnressn  5606  fressnfv  5607  fvtp2g  5629  fvtp3g  5630  fnex  5642  funfvima3  5651  isores3  5716  f1o2ndf1  6125  reldmtpos  6150  smores  6189  tfrlem7  6214  tfrlemi1  6229  tfrexlem  6231  tfrcl  6261  frecrdg  6305  nnacl  6376  nnmcl  6377  nnmsucr  6384  nntri3or  6389  nnaword  6407  nnaordex  6423  2ecoptocl  6517  ssct  6712  enm  6714  xpf1o  6738  ac6sfi  6792  f1dmvrnfibi  6832  f1vrnfibi  6833  updjud  6967  enumct  7000  elni2  7122  ax1rid  7685  negf1o  8144  mulgt1  8621  lbreu  8703  nnaddcl  8740  nnmulcl  8741  zaddcllempos  9091  zaddcllemneg  9093  nn0n0n1ge2b  9130  fzind  9166  fnn0ind  9167  uzaddcl  9381  uzsubsubfz  9827  elfz1b  9870  elfz0ubfz0  9902  fz0fzdiffz0  9907  elfzmlbp  9909  fzofzim  9965  elfzom1elp1fzo  9979  elfzom1p1elfzo  9991  ssfzo12bi  10002  modfzo0difsn  10168  seq3val  10231  seqvalcd  10232  expcllem  10304  expap0  10323  faclbnd  10487  faclbnd6  10490  fihashf1rn  10535  omgadd  10548  hashfzp1  10570  seq3coll  10585  cjexp  10665  r19.29uz  10764  resqrexlemover  10782  resqrexlemlo  10785  resqrexlemcalc3  10788  absexp  10851  fimaxre2  10998  climshft  11073  climub  11113  climserle  11114  sumfct  11143  isumss2  11162  binom  11253  bcxmas  11258  clim2prod  11308  prodfap0  11314  prodfrecap  11315  demoivreALT  11480  dvdsdivcl  11548  dvdsfac  11558  oddnn02np1  11577  oddge22np1  11578  evennn02n  11579  evennn2n  11580  m1exp1  11598  nn0o  11604  flodddiv4  11631  gcdneg  11670  bezoutlemmain  11686  dfgcd2  11702  gcdmultiple  11708  alginv  11728  cncongr1  11784  prmdvdsexp  11826  prmndvdsfaclt  11834  clsss  12287  xmettri2  12530  mettri  12542  metss  12663  bdssexg  13102  bj-findis  13177  nninfalllemn  13202  nninfalllem1  13203  nninfsellemdc  13206