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  1699  19.41  1700  equtr2  1725  mopick  2123  2euex  2132  gencl  2795  2gencl  2796  rspccva  2867  indifdir  3419  sseq0  3492  minel  3512  r19.2m  3537  r19.2mOLD  3538  elelpwi  3617  ssuni  3861  disjiun  4028  trintssm  4147  ssexg  4172  pofun  4347  sowlin  4355  2optocl  4740  3optocl  4741  elrnmpt1  4917  resieq  4956  fnun  5364  fss  5419  fun  5430  dmfex  5447  fvelimab  5617  mptfvex  5647  fmptco  5728  fnressn  5748  fressnfv  5749  fvtp2g  5771  fvtp3g  5772  fnex  5784  funfvima3  5796  isores3  5862  f1o2ndf1  6286  reldmtpos  6311  smores  6350  tfrlem7  6375  tfrlemi1  6390  tfrexlem  6392  tfrcl  6422  frecrdg  6466  nnacl  6538  nnmcl  6539  nnmsucr  6546  nntri3or  6551  nnaword  6569  nnaordex  6586  2ecoptocl  6682  ssct  6877  enm  6879  xpf1o  6905  ac6sfi  6959  f1dmvrnfibi  7010  f1vrnfibi  7011  updjud  7148  enumct  7181  nnnninfeq  7194  exmidontriimlem4  7291  exmidontriim  7292  elni2  7381  ax1rid  7944  negf1o  8408  mulgt1  8890  lbreu  8972  nnaddcl  9010  nnmulcl  9011  zaddcllempos  9363  zaddcllemneg  9365  nn0n0n1ge2b  9405  fzind  9441  fnn0ind  9442  uzaddcl  9660  elpq  9723  uzsubsubfz  10122  elfz1b  10165  elfz0ubfz0  10200  fz0fzdiffz0  10205  elfzmlbp  10207  fzofzim  10264  elfzom1elp1fzo  10278  elfzom1p1elfzo  10290  ssfzo12bi  10301  modfzo0difsn  10487  seq3val  10552  seqvalcd  10553  expcllem  10642  expap0  10661  apexp1  10810  faclbnd  10833  faclbnd6  10836  fihashf1rn  10880  omgadd  10894  hashfzp1  10916  seq3coll  10934  cjexp  11058  r19.29uz  11157  resqrexlemover  11175  resqrexlemlo  11178  resqrexlemcalc3  11181  absexp  11244  fimaxre2  11392  climshft  11469  climub  11509  climserle  11510  sumfct  11539  isumss2  11558  binom  11649  bcxmas  11654  clim2prod  11704  prodfap0  11710  prodfrecap  11711  prodfct  11752  demoivreALT  11939  dvdsdivcl  12015  dvdsfac  12025  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  m1exp1  12066  nn0o  12072  flodddiv4  12101  gcdneg  12149  bezoutlemmain  12165  dfgcd2  12181  gcdmultiple  12187  nnwosdc  12206  alginv  12215  cncongr1  12271  prmdvdsexp  12316  prmndvdsfaclt  12324  dfgrp2  13159  srgmulgass  13545  lmodvsmmulgdi  13879  lmodfopnelem1  13880  rmodislmodlem  13906  cnfldmulg  14132  cnfldexp  14133  clsss  14354  xmettri2  14597  mettri  14609  metss  14730  plycolemc  14994  zabsle1  15240  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem3  15304  gausslemma2dlem4  15305  2lgslem1a1  15327  bdssexg  15550  bj-findis  15625  nninfalllem1  15652  nninfsellemdc  15654  redc0  15701