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  2833  2gencl  2834  vtocl4g  2873  vtocl4ga  2874  rspccva  2907  indifdir  3461  sseq0  3534  minel  3554  r19.2m  3579  r19.2mOLD  3580  elelpwi  3662  ssuni  3913  disjiun  4081  trintssm  4201  ssexg  4226  pofun  4407  sowlin  4415  2optocl  4801  3optocl  4802  ssrelrn  4920  elrnmpt1  4981  resieq  5021  fnun  5435  fss  5491  fun  5505  dmfex  5523  fvelimab  5698  mptfvex  5728  fmptco  5809  fnressn  5835  fressnfv  5836  fvtp2g  5858  fvtp3g  5859  fnex  5871  funfvima3  5883  isores3  5951  f1o2ndf1  6388  reldmtpos  6414  smores  6453  tfrlem7  6478  tfrlemi1  6493  tfrexlem  6495  tfrcl  6525  frecrdg  6569  nnacl  6643  nnmcl  6644  nnmsucr  6651  nntri3or  6656  nnaword  6674  nnaordex  6691  2ecoptocl  6787  ssct  6995  enm  6999  xpf1o  7025  ac6sfi  7080  f1dmvrnfibi  7134  f1vrnfibi  7135  updjud  7272  enumct  7305  nnnninfeq  7318  exmidontriimlem4  7429  exmidontriim  7430  elni2  7524  ax1rid  8087  negf1o  8551  mulgt1  9033  lbreu  9115  nnaddcl  9153  nnmulcl  9154  zaddcllempos  9506  zaddcllemneg  9508  nn0n0n1ge2b  9549  fzind  9585  fnn0ind  9586  uzaddcl  9810  elpq  9873  uzsubsubfz  10272  elfz1b  10315  elfz0ubfz0  10350  fz0fzdiffz0  10355  elfzmlbp  10357  fzofzim  10417  elfzom1elp1fzo  10437  elfzom1p1elfzo  10449  ssfzo12bi  10460  modfzo0difsn  10647  seq3val  10712  seqvalcd  10713  expcllem  10802  expap0  10821  apexp1  10970  faclbnd  10993  faclbnd6  10996  fihashf1rn  11040  omgadd  11055  hashfzp1  11078  seq3coll  11096  fundm2domnop0  11099  lswlgt0cl  11156  ccatsymb  11169  swrdnd  11230  swrd0g  11231  swrdspsleq  11238  pfxsuff1eqwrdeq  11270  swrdswrdlem  11275  swrdswrd  11276  wrd2ind  11294  pfxccatin12lem2a  11298  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  pfxccat3a  11309  swrdccat3blem  11310  cjexp  11444  r19.29uz  11543  resqrexlemover  11561  resqrexlemlo  11564  resqrexlemcalc3  11567  absexp  11630  fimaxre2  11778  climshft  11855  climub  11895  climserle  11896  sumfct  11925  isumss2  11944  binom  12035  bcxmas  12040  clim2prod  12090  prodfap0  12096  prodfrecap  12097  prodfct  12138  demoivreALT  12325  dvdsdivcl  12401  dvdsfac  12411  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  m1exp1  12452  nn0o  12458  flodddiv4  12487  gcdneg  12543  bezoutlemmain  12559  dfgcd2  12575  gcdmultiple  12581  nnwosdc  12600  alginv  12609  cncongr1  12665  prmdvdsexp  12710  prmndvdsfaclt  12718  dfgrp2  13600  srgmulgass  13992  lmodvsmmulgdi  14327  lmodfopnelem1  14328  rmodislmodlem  14354  cnfldmulg  14580  cnfldexp  14581  clsss  14832  xmettri2  15075  mettri  15087  metss  15208  plycolemc  15472  zabsle1  15718  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem3  15782  gausslemma2dlem4  15783  2lgslem1a1  15805  incistruhgr  15931  umgrislfupgrenlem  15969  uhgr2edg  16045  usgredg2vlem2  16062  wlkl1loop  16155  wlkres  16174  clwwlkccatlem  16195  isclwwlknx  16211  clwwlkext2edg  16217  clwwlknonel  16227  clwwlknonex2lem2  16233  clwwlknun  16236  bdssexg  16435  bj-findis  16510  nninfalllem1  16546  nninfsellemdc  16548  redc0  16597