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  2159  2euex  2168  gencl  2845  2gencl  2846  vtocl4g  2885  vtocl4ga  2886  rspccva  2919  indifdir  3476  sseq0  3549  minel  3569  r19.2m  3595  r19.2mOLD  3596  elelpwi  3680  ssuni  3935  disjiun  4103  trintssm  4223  ssexg  4248  pofun  4432  sowlin  4440  2optocl  4826  3optocl  4827  ssrelrn  4946  elrnmpt1  5007  resieq  5047  fnun  5463  fss  5520  fun  5535  dmfex  5556  fvelimab  5732  mptfvex  5762  fmptco  5842  fnressn  5869  fressnfv  5870  fvtp2g  5892  fvtp3g  5893  fnex  5905  funfvima3  5919  isores3  5987  f1o2ndf1  6423  funsssuppss  6457  reldmtpos  6483  smores  6522  tfrlem7  6547  tfrlemi1  6562  tfrexlem  6564  tfrcl  6594  frecrdg  6638  nnacl  6712  nnmcl  6713  nnmsucr  6720  nntri3or  6725  nnaword  6743  nnaordex  6760  2ecoptocl  6856  ssct  7066  enm  7070  xpf1o  7096  ac6sfi  7154  f1dmvrnfibi  7210  f1vrnfibi  7211  suppeqfsuppbi  7247  updjud  7372  enumct  7405  nnnninfeq  7418  exmidontriimlem4  7530  exmidontriim  7531  elni2  7628  ax1rid  8191  negf1o  8654  mulgt1  9136  lbreu  9218  nnaddcl  9256  nnmulcl  9257  zaddcllempos  9613  zaddcllemneg  9615  nn0n0n1ge2b  9656  fzind  9692  fnn0ind  9693  uzaddcl  9917  elpq  9980  uzsubsubfz  10380  elfz1b  10423  elfz0ubfz0  10458  fz0fzdiffz0  10463  elfzmlbp  10465  fzofzim  10526  elfzom1elp1fzo  10546  elfzom1p1elfzo  10558  ssfzo12bi  10569  modfzo0difsn  10756  seq3val  10821  seqvalcd  10822  expcllem  10911  expap0  10930  apexp1  11079  faclbnd  11102  faclbnd6  11105  fihashf1rn  11149  omgadd  11164  hashfzp1  11187  seq3coll  11210  fundm2domnop0  11216  lswlgt0cl  11273  ccatsymb  11286  swrdnd  11347  swrd0g  11348  swrdspsleq  11355  pfxsuff1eqwrdeq  11387  swrdswrdlem  11392  swrdswrd  11393  wrd2ind  11411  pfxccatin12lem2a  11415  swrdccatin2  11417  pfxccatin12lem2  11419  pfxccatin12lem3  11420  pfxccatin12  11421  pfxccat3  11422  swrdccat  11423  pfxccat3a  11426  swrdccat3blem  11427  cjexp  11574  r19.29uz  11673  resqrexlemover  11691  resqrexlemlo  11694  resqrexlemcalc3  11697  absexp  11760  fimaxre2  11908  climshft  11985  climub  12025  climserle  12026  sumfct  12055  isumss2  12075  binom  12166  bcxmas  12171  clim2prod  12221  prodfap0  12227  prodfrecap  12228  prodfct  12269  demoivreALT  12456  dvdsdivcl  12532  dvdsfac  12542  oddnn02np1  12562  oddge22np1  12563  evennn02n  12564  evennn2n  12565  m1exp1  12583  nn0o  12589  flodddiv4  12618  gcdneg  12674  bezoutlemmain  12690  dfgcd2  12706  gcdmultiple  12712  nnwosdc  12731  alginv  12740  cncongr1  12796  prmdvdsexp  12841  prmndvdsfaclt  12849  dfgrp2  13732  srgmulgass  14125  lmodvsmmulgdi  14463  lmodfopnelem1  14464  rmodislmodlem  14490  cnfldmulg  14716  cnfldexp  14717  clsss  14975  xmettri2  15218  mettri  15230  metss  15351  plycolemc  15615  zabsle1  15864  gausslemma2dlem1a  15923  gausslemma2dlem2  15927  gausslemma2dlem3  15928  gausslemma2dlem4  15929  2lgslem1a1  15951  incistruhgr  16077  umgrislfupgrenlem  16117  uhgr2edg  16193  usgredg2vlem2  16210  subgrfun  16254  wlkl1loop  16345  wlkres  16366  clwwlkccatlem  16387  isclwwlknx  16403  clwwlkext2edg  16409  clwwlknonel  16419  clwwlknonex2lem2  16425  clwwlknun  16428  depindlem2  16494  depindlem3  16495  bdssexg  16666  bj-findis  16741  nninfalllem1  16778  nninfsellemdc  16780  redc0  16834