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  1685  19.41  1686  equtr2  1711  mopick  2104  2euex  2113  gencl  2771  2gencl  2772  rspccva  2842  indifdir  3393  sseq0  3466  minel  3486  r19.2m  3511  r19.2mOLD  3512  elelpwi  3589  ssuni  3833  disjiun  4000  trintssm  4119  ssexg  4144  pofun  4314  sowlin  4322  2optocl  4705  3optocl  4706  elrnmpt1  4880  resieq  4919  fnun  5324  fss  5379  fun  5390  dmfex  5407  fvelimab  5574  mptfvex  5603  fmptco  5684  fnressn  5704  fressnfv  5705  fvtp2g  5727  fvtp3g  5728  fnex  5740  funfvima3  5752  isores3  5818  f1o2ndf1  6231  reldmtpos  6256  smores  6295  tfrlem7  6320  tfrlemi1  6335  tfrexlem  6337  tfrcl  6367  frecrdg  6411  nnacl  6483  nnmcl  6484  nnmsucr  6491  nntri3or  6496  nnaword  6514  nnaordex  6531  2ecoptocl  6625  ssct  6820  enm  6822  xpf1o  6846  ac6sfi  6900  f1dmvrnfibi  6945  f1vrnfibi  6946  updjud  7083  enumct  7116  nnnninfeq  7128  exmidontriimlem4  7225  exmidontriim  7226  elni2  7315  ax1rid  7878  negf1o  8341  mulgt1  8822  lbreu  8904  nnaddcl  8941  nnmulcl  8942  zaddcllempos  9292  zaddcllemneg  9294  nn0n0n1ge2b  9334  fzind  9370  fnn0ind  9371  uzaddcl  9588  elpq  9650  uzsubsubfz  10049  elfz1b  10092  elfz0ubfz0  10127  fz0fzdiffz0  10132  elfzmlbp  10134  fzofzim  10190  elfzom1elp1fzo  10204  elfzom1p1elfzo  10216  ssfzo12bi  10227  modfzo0difsn  10397  seq3val  10460  seqvalcd  10461  expcllem  10533  expap0  10552  apexp1  10700  faclbnd  10723  faclbnd6  10726  fihashf1rn  10770  omgadd  10784  hashfzp1  10806  seq3coll  10824  cjexp  10904  r19.29uz  11003  resqrexlemover  11021  resqrexlemlo  11024  resqrexlemcalc3  11027  absexp  11090  fimaxre2  11237  climshft  11314  climub  11354  climserle  11355  sumfct  11384  isumss2  11403  binom  11494  bcxmas  11499  clim2prod  11549  prodfap0  11555  prodfrecap  11556  prodfct  11597  demoivreALT  11783  dvdsdivcl  11858  dvdsfac  11868  oddnn02np1  11887  oddge22np1  11888  evennn02n  11889  evennn2n  11890  m1exp1  11908  nn0o  11914  flodddiv4  11941  gcdneg  11985  bezoutlemmain  12001  dfgcd2  12017  gcdmultiple  12023  nnwosdc  12042  alginv  12049  cncongr1  12105  prmdvdsexp  12150  prmndvdsfaclt  12158  dfgrp2  12907  srgmulgass  13177  lmodvsmmulgdi  13418  lmodfopnelem1  13419  rmodislmodlem  13445  cnfldmulg  13509  cnfldexp  13510  clsss  13657  xmettri2  13900  mettri  13912  metss  14033  zabsle1  14439  bdssexg  14695  bj-findis  14770  nninfalllem1  14796  nninfsellemdc  14798  redc0  14844