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  4245  ssexg  4272  pofun  4457  sowlin  4465  2optocl  4852  3optocl  4853  ssrelrn  4972  elrnmpt1  5033  resieq  5073  fnun  5489  fss  5546  fun  5561  dmfex  5582  fvelimab  5759  mptfvex  5791  fmptco  5874  fnressn  5901  fressnfv  5902  fvtp2g  5924  fvtp3g  5925  fnex  5937  funfvima3  5952  isores3  6021  f1o2ndf1  6464  funsssuppss  6498  reldmtpos  6524  smores  6563  tfrlem7  6588  tfrlemi1  6603  tfrexlem  6605  tfrcl  6635  frecrdg  6679  nnacl  6753  nnmcl  6754  nnmsucr  6761  nntri3or  6766  nnaword  6784  nnaordex  6801  2ecoptocl  6897  ssct  7114  enm  7118  xpf1o  7144  ac6sfi  7202  f1dmvrnfibi  7258  f1vrnfibi  7259  suppeqfsuppbi  7295  updjud  7423  enumct  7456  nnnninfeq  7469  exmidontriimlem4  7581  exmidontriim  7582  elni2  7682  ax1rid  8245  negf1o  8711  mulgt1  9196  lbreu  9278  nnaddcl  9327  nnmulcl  9328  zaddcllempos  9686  zaddcllemneg  9688  nn0n0n1ge2b  9730  fzind  9766  fnn0ind  9767  uzaddcl  9996  elpq  10060  uzsubsubfz  10463  elfz1b  10508  elfz0ubfz0  10543  fz0fzdiffz0  10548  elfzmlbp  10550  fzofzim  10611  elfzom1elp1fzo  10631  elfzom1p1elfzo  10643  ssfzo12bi  10654  modfzo0difsn  10847  seq3val  10912  seqvalcd  10913  expcllem  11002  expap0  11021  apexp1  11172  faclbnd  11195  faclbnd6  11198  fihashf1rn  11243  omgadd  11258  hashfzp1  11281  hashmap  11284  seq3coll  11310  fundm2domnop0  11316  lswlgt0cl  11373  ccatsymb  11386  swrdnd  11447  swrd0g  11448  swrdspsleq  11455  pfxsuff1eqwrdeq  11487  swrdswrdlem  11492  swrdswrd  11493  wrd2ind  11511  pfxccatin12lem2a  11515  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  pfxccat3a  11526  swrdccat3blem  11527  cjexp  11674  r19.29uz  11774  resqrexlemover  11792  resqrexlemlo  11795  resqrexlemcalc3  11798  absexp  11862  fimaxre2  12010  climshft  12089  climub  12129  climserle  12130  sumfct  12159  isumss2  12179  binom  12270  bcxmas  12275  clim2prod  12325  prodfap0  12331  prodfrecap  12332  prodfct  12373  demoivreALT  12560  dvdsdivcl  12636  dvdsfac  12646  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  m1exp1  12687  nn0o  12693  flodddiv4  12722  gcdneg  12778  bezoutlemmain  12794  dfgcd2  12810  gcdmultiple  12816  nnwosdc  12835  alginv  12844  cncongr1  12900  prmdvdsexp  12946  prmndvdsfaclt  12954  dfgrp2  13885  srgmulgass  14377  lmodvsmmulgdi  14744  lmodfopnelem1  14745  rmodislmodlem  14771  cnfldmulg  14997  cnfldexp  14998  assamulgscm  15127  clsss  15310  xmettri2  15553  mettri  15565  metss  15686  plycolemc  15950  zabsle1  16284  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem3  16348  gausslemma2dlem4  16349  2lgslem1a1  16371  incistruhgr  16497  umgrislfupgrenlem  16537  uhgr2edg  16613  usgredg2vlem2  16630  subgrfun  16674  wlkl1loop  16765  wlkres  16786  clwwlkccatlem  16807  isclwwlknx  16823  clwwlkext2edg  16829  clwwlknonel  16839  clwwlknonex2lem2  16845  clwwlknun  16848  depindlem2  16914  depindlem3  16915  bdssexg  17096  bj-findis  17171  nninfalllem1  17217  nninfsellemdc  17219  redc0  17274