Theorem impcom 124

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  mpan9  279  19.41h  1678  19.41  1679  equtr2  1704  mopick  2097  2euex  2106  gencl  2762  2gencl  2763  rspccva  2833  indifdir  3383  sseq0  3456  minel  3476  r19.2m  3501  r19.2mOLD  3502  elelpwi  3578  ssuni  3818  disjiun  3984  trintssm  4103  ssexg  4128  pofun  4297  sowlin  4305  2optocl  4688  3optocl  4689  elrnmpt1  4862  resieq  4901  fnun  5304  fss  5359  fun  5370  dmfex  5387  fvelimab  5552  mptfvex  5581  fmptco  5662  fnressn  5682  fressnfv  5683  fvtp2g  5705  fvtp3g  5706  fnex  5718  funfvima3  5729  isores3  5794  f1o2ndf1  6207  reldmtpos  6232  smores  6271  tfrlem7  6296  tfrlemi1  6311  tfrexlem  6313  tfrcl  6343  frecrdg  6387  nnacl  6459  nnmcl  6460  nnmsucr  6467  nntri3or  6472  nnaword  6490  nnaordex  6507  2ecoptocl  6601  ssct  6796  enm  6798  xpf1o  6822  ac6sfi  6876  f1dmvrnfibi  6921  f1vrnfibi  6922  updjud  7059  enumct  7092  nnnninfeq  7104  exmidontriimlem4  7201  exmidontriim  7202  elni2  7276  ax1rid  7839  negf1o  8301  mulgt1  8779  lbreu  8861  nnaddcl  8898  nnmulcl  8899  zaddcllempos  9249  zaddcllemneg  9251  nn0n0n1ge2b  9291  fzind  9327  fnn0ind  9328  uzaddcl  9545  elpq  9607  uzsubsubfz  10003  elfz1b  10046  elfz0ubfz0  10081  fz0fzdiffz0  10086  elfzmlbp  10088  fzofzim  10144  elfzom1elp1fzo  10158  elfzom1p1elfzo  10170  ssfzo12bi  10181  modfzo0difsn  10351  seq3val  10414  seqvalcd  10415  expcllem  10487  expap0  10506  apexp1  10652  faclbnd  10675  faclbnd6  10678  fihashf1rn  10723  omgadd  10737  hashfzp1  10759  seq3coll  10777  cjexp  10857  r19.29uz  10956  resqrexlemover  10974  resqrexlemlo  10977  resqrexlemcalc3  10980  absexp  11043  fimaxre2  11190  climshft  11267  climub  11307  climserle  11308  sumfct  11337  isumss2  11356  binom  11447  bcxmas  11452  clim2prod  11502  prodfap0  11508  prodfrecap  11509  prodfct  11550  demoivreALT  11736  dvdsdivcl  11810  dvdsfac  11820  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  m1exp1  11860  nn0o  11866  flodddiv4  11893  gcdneg  11937  bezoutlemmain  11953  dfgcd2  11969  gcdmultiple  11975  nnwosdc  11994  alginv  12001  cncongr1  12057  prmdvdsexp  12102  prmndvdsfaclt  12110  dfgrp2  12732  clsss  12912  xmettri2  13155  mettri  13167  metss  13288  zabsle1  13694  bdssexg  13939  bj-findis  14014  nninfalllem1  14041  nninfsellemdc  14043  redc0  14089