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  1733  19.41  1734  equtr2  1759  mopick  2158  2euex  2167  gencl  2835  2gencl  2836  vtocl4g  2875  vtocl4ga  2876  rspccva  2909  indifdir  3463  sseq0  3536  minel  3556  r19.2m  3581  r19.2mOLD  3582  elelpwi  3664  ssuni  3915  disjiun  4083  trintssm  4203  ssexg  4228  pofun  4409  sowlin  4417  2optocl  4803  3optocl  4804  ssrelrn  4922  elrnmpt1  4983  resieq  5023  fnun  5438  fss  5494  fun  5508  dmfex  5526  fvelimab  5702  mptfvex  5732  fmptco  5813  fnressn  5840  fressnfv  5841  fvtp2g  5863  fvtp3g  5864  fnex  5876  funfvima3  5888  isores3  5956  f1o2ndf1  6393  reldmtpos  6419  smores  6458  tfrlem7  6483  tfrlemi1  6498  tfrexlem  6500  tfrcl  6530  frecrdg  6574  nnacl  6648  nnmcl  6649  nnmsucr  6656  nntri3or  6661  nnaword  6679  nnaordex  6696  2ecoptocl  6792  ssct  7000  enm  7004  xpf1o  7030  ac6sfi  7087  f1dmvrnfibi  7143  f1vrnfibi  7144  updjud  7281  enumct  7314  nnnninfeq  7327  exmidontriimlem4  7439  exmidontriim  7440  elni2  7534  ax1rid  8097  negf1o  8561  mulgt1  9043  lbreu  9125  nnaddcl  9163  nnmulcl  9164  zaddcllempos  9516  zaddcllemneg  9518  nn0n0n1ge2b  9559  fzind  9595  fnn0ind  9596  uzaddcl  9820  elpq  9883  uzsubsubfz  10282  elfz1b  10325  elfz0ubfz0  10360  fz0fzdiffz0  10365  elfzmlbp  10367  fzofzim  10428  elfzom1elp1fzo  10448  elfzom1p1elfzo  10460  ssfzo12bi  10471  modfzo0difsn  10658  seq3val  10723  seqvalcd  10724  expcllem  10813  expap0  10832  apexp1  10981  faclbnd  11004  faclbnd6  11007  fihashf1rn  11051  omgadd  11066  hashfzp1  11089  seq3coll  11107  fundm2domnop0  11113  lswlgt0cl  11170  ccatsymb  11183  swrdnd  11244  swrd0g  11245  swrdspsleq  11252  pfxsuff1eqwrdeq  11284  swrdswrdlem  11289  swrdswrd  11290  wrd2ind  11308  pfxccatin12lem2a  11312  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccat3a  11323  swrdccat3blem  11324  cjexp  11458  r19.29uz  11557  resqrexlemover  11575  resqrexlemlo  11578  resqrexlemcalc3  11581  absexp  11644  fimaxre2  11792  climshft  11869  climub  11909  climserle  11910  sumfct  11939  isumss2  11959  binom  12050  bcxmas  12055  clim2prod  12105  prodfap0  12111  prodfrecap  12112  prodfct  12153  demoivreALT  12340  dvdsdivcl  12416  dvdsfac  12426  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  m1exp1  12467  nn0o  12473  flodddiv4  12502  gcdneg  12558  bezoutlemmain  12574  dfgcd2  12590  gcdmultiple  12596  nnwosdc  12615  alginv  12624  cncongr1  12680  prmdvdsexp  12725  prmndvdsfaclt  12733  dfgrp2  13615  srgmulgass  14008  lmodvsmmulgdi  14343  lmodfopnelem1  14344  rmodislmodlem  14370  cnfldmulg  14596  cnfldexp  14597  clsss  14848  xmettri2  15091  mettri  15103  metss  15224  plycolemc  15488  zabsle1  15734  gausslemma2dlem1a  15793  gausslemma2dlem2  15797  gausslemma2dlem3  15798  gausslemma2dlem4  15799  2lgslem1a1  15821  incistruhgr  15947  umgrislfupgrenlem  15987  uhgr2edg  16063  usgredg2vlem2  16080  subgrfun  16124  wlkl1loop  16215  wlkres  16236  clwwlkccatlem  16257  isclwwlknx  16273  clwwlkext2edg  16279  clwwlknonel  16289  clwwlknonex2lem2  16295  clwwlknun  16298  depindlem2  16352  depindlem3  16353  bdssexg  16525  bj-findis  16600  nninfalllem1  16636  nninfsellemdc  16638  redc0  16688