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  1731  19.41  1732  equtr2  1757  mopick  2156  2euex  2165  gencl  2832  2gencl  2833  vtocl4g  2872  vtocl4ga  2873  rspccva  2906  indifdir  3460  sseq0  3533  minel  3553  r19.2m  3578  r19.2mOLD  3579  elelpwi  3661  ssuni  3909  disjiun  4077  trintssm  4197  ssexg  4222  pofun  4402  sowlin  4410  2optocl  4795  3optocl  4796  ssrelrn  4913  elrnmpt1  4974  resieq  5014  fnun  5428  fss  5484  fun  5496  dmfex  5514  fvelimab  5689  mptfvex  5719  fmptco  5800  fnressn  5824  fressnfv  5825  fvtp2g  5847  fvtp3g  5848  fnex  5860  funfvima3  5872  isores3  5938  f1o2ndf1  6372  reldmtpos  6397  smores  6436  tfrlem7  6461  tfrlemi1  6476  tfrexlem  6478  tfrcl  6508  frecrdg  6552  nnacl  6624  nnmcl  6625  nnmsucr  6632  nntri3or  6637  nnaword  6655  nnaordex  6672  2ecoptocl  6768  ssct  6973  enm  6975  xpf1o  7001  ac6sfi  7056  f1dmvrnfibi  7107  f1vrnfibi  7108  updjud  7245  enumct  7278  nnnninfeq  7291  exmidontriimlem4  7402  exmidontriim  7403  elni2  7497  ax1rid  8060  negf1o  8524  mulgt1  9006  lbreu  9088  nnaddcl  9126  nnmulcl  9127  zaddcllempos  9479  zaddcllemneg  9481  nn0n0n1ge2b  9522  fzind  9558  fnn0ind  9559  uzaddcl  9777  elpq  9840  uzsubsubfz  10239  elfz1b  10282  elfz0ubfz0  10317  fz0fzdiffz0  10322  elfzmlbp  10324  fzofzim  10384  elfzom1elp1fzo  10403  elfzom1p1elfzo  10415  ssfzo12bi  10426  modfzo0difsn  10612  seq3val  10677  seqvalcd  10678  expcllem  10767  expap0  10786  apexp1  10935  faclbnd  10958  faclbnd6  10961  fihashf1rn  11005  omgadd  11019  hashfzp1  11041  seq3coll  11059  fundm2domnop0  11062  lswlgt0cl  11119  ccatsymb  11132  swrdnd  11186  swrd0g  11187  swrdspsleq  11194  pfxsuff1eqwrdeq  11226  swrdswrdlem  11231  swrdswrd  11232  wrd2ind  11250  pfxccatin12lem2a  11254  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  pfxccat3a  11265  swrdccat3blem  11266  cjexp  11399  r19.29uz  11498  resqrexlemover  11516  resqrexlemlo  11519  resqrexlemcalc3  11522  absexp  11585  fimaxre2  11733  climshft  11810  climub  11850  climserle  11851  sumfct  11880  isumss2  11899  binom  11990  bcxmas  11995  clim2prod  12045  prodfap0  12051  prodfrecap  12052  prodfct  12093  demoivreALT  12280  dvdsdivcl  12356  dvdsfac  12366  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  m1exp1  12407  nn0o  12413  flodddiv4  12442  gcdneg  12498  bezoutlemmain  12514  dfgcd2  12530  gcdmultiple  12536  nnwosdc  12555  alginv  12564  cncongr1  12620  prmdvdsexp  12665  prmndvdsfaclt  12673  dfgrp2  13555  srgmulgass  13947  lmodvsmmulgdi  14281  lmodfopnelem1  14282  rmodislmodlem  14308  cnfldmulg  14534  cnfldexp  14535  clsss  14786  xmettri2  15029  mettri  15041  metss  15162  plycolemc  15426  zabsle1  15672  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem3  15736  gausslemma2dlem4  15737  2lgslem1a1  15759  incistruhgr  15884  umgrislfupgrenlem  15922  uhgr2edg  15998  usgredg2vlem2  16015  bdssexg  16225  bj-findis  16300  nninfalllem1  16333  nninfsellemdc  16335  redc0  16384