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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  mpan9  281  19.41h  1737  19.41  1738  equtr2  1763  mopick  2165  2euex  2174  gencl  2854  2gencl  2855  vtocl4g  2894  vtocl4ga  2895  rspccva  2928  indifdir  3487  minel  3586  r19.2m  3614  r19.2mOLD  3615  elelpwi  3701  ssuni  3957  disjiun  4125  trintssm  4247  ssexg  4274  pofun  4459  sowlin  4467  2optocl  4854  3optocl  4855  ssrelrn  4974  elrnmpt1  5035  resieq  5075  fnun  5492  fss  5549  fun  5564  dmfex  5585  fvelimab  5762  mptfvex  5794  fmptco  5877  fnressn  5904  fressnfv  5905  fvtp2g  5927  fvtp3g  5928  fnex  5940  funfvima3  5955  isores3  6024  f1o2ndf1  6468  funsssuppss  6502  reldmtpos  6528  smores  6567  tfrlem7  6592  tfrlemi1  6607  tfrexlem  6609  tfrcl  6639  frecrdg  6683  nnacl  6757  nnmcl  6758  nnmsucr  6765  nntri3or  6770  nnaword  6788  nnaordex  6805  2ecoptocl  6901  ssct  7118  enm  7122  xpf1o  7148  ac6sfi  7206  f1dmvrnfibi  7262  f1vrnfibi  7263  suppeqfsuppbi  7300  updjud  7428  enumct  7461  nnnninfeq  7474  exmidontriimlem4  7586  exmidontriim  7587  elni2  7687  ax1rid  8250  negf1o  8716  mulgt1  9201  lbreu  9283  nnaddcl  9333  nnmulcl  9334  zaddcllempos  9692  zaddcllemneg  9694  nn0n0n1ge2b  9736  fzind  9772  fnn0ind  9773  uzaddcl  10002  elpq  10066  uzsubsubfz  10469  elfz1b  10514  elfz0ubfz0  10549  fz0fzdiffz0  10554  elfzmlbp  10556  fzofzim  10617  elfzom1elp1fzo  10637  elfzom1p1elfzo  10649  ssfzo12bi  10660  modfzo0difsn  10853  seq3val  10918  seqvalcd  10919  expcllem  11008  expap0  11027  apexp1  11178  faclbnd  11201  faclbnd6  11204  fihashf1rn  11249  omgadd  11264  hashfzp1  11287  hashmap  11290  seq3coll  11316  fundm2domnop0  11322  lswlgt0cl  11379  ccatsymb  11392  swrdnd  11453  swrd0g  11454  swrdspsleq  11461  pfxsuff1eqwrdeq  11493  swrdswrdlem  11498  swrdswrd  11499  wrd2ind  11517  pfxccatin12lem2a  11521  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  pfxccat3a  11532  swrdccat3blem  11533  cjexp  11680  r19.29uz  11780  resqrexlemover  11798  resqrexlemlo  11801  resqrexlemcalc3  11804  absexp  11868  fimaxre2  12016  climshft  12095  climub  12135  climserle  12136  sumfct  12165  isumss2  12185  binom  12276  bcxmas  12281  clim2prod  12331  prodfap0  12337  prodfrecap  12338  prodfct  12379  demoivreALT  12566  dvdsdivcl  12642  dvdsfac  12652  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  m1exp1  12693  nn0o  12699  flodddiv4  12728  gcdneg  12784  bezoutlemmain  12800  dfgcd2  12816  gcdmultiple  12822  nnwosdc  12841  alginv  12850  cncongr1  12906  prmdvdsexp  12952  prmndvdsfaclt  12960  dfgrp2  13891  srgmulgass  14400  lmodvsmmulgdi  14769  lmodfopnelem1  14770  rmodislmodlem  14796  cnfldmulg  15022  cnfldexp  15023  assamulgscm  15152  clsss  15344  xmettri2  15587  mettri  15599  metss  15720  plycolemc  15984  zabsle1  16323  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem3  16387  gausslemma2dlem4  16388  2lgslem1a1  16410  incistruhgr  16536  umgrislfupgrenlem  16576  uhgr2edg  16652  usgredg2vlem2  16669  subgrfun  16713  wlkl1loop  16804  wlkres  16825  clwwlkccatlem  16846  isclwwlknx  16862  clwwlkext2edg  16868  clwwlknonel  16878  clwwlknonex2lem2  16884  clwwlknun  16887  depindlem2  16953  depindlem3  16954  bdssexg  17135  bj-findis  17210  nninfalllem1  17257  nninfsellemdc  17259  redc0  17314