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  1696  19.41  1697  equtr2  1722  mopick  2116  2euex  2125  gencl  2784  2gencl  2785  rspccva  2855  indifdir  3406  sseq0  3479  minel  3499  r19.2m  3524  r19.2mOLD  3525  elelpwi  3602  ssuni  3846  disjiun  4013  trintssm  4132  ssexg  4157  pofun  4330  sowlin  4338  2optocl  4721  3optocl  4722  elrnmpt1  4896  resieq  4935  fnun  5341  fss  5396  fun  5407  dmfex  5424  fvelimab  5592  mptfvex  5621  fmptco  5702  fnressn  5722  fressnfv  5723  fvtp2g  5745  fvtp3g  5746  fnex  5758  funfvima3  5770  isores3  5836  f1o2ndf1  6252  reldmtpos  6277  smores  6316  tfrlem7  6341  tfrlemi1  6356  tfrexlem  6358  tfrcl  6388  frecrdg  6432  nnacl  6504  nnmcl  6505  nnmsucr  6512  nntri3or  6517  nnaword  6535  nnaordex  6552  2ecoptocl  6648  ssct  6843  enm  6845  xpf1o  6871  ac6sfi  6925  f1dmvrnfibi  6972  f1vrnfibi  6973  updjud  7110  enumct  7143  nnnninfeq  7155  exmidontriimlem4  7252  exmidontriim  7253  elni2  7342  ax1rid  7905  negf1o  8368  mulgt1  8849  lbreu  8931  nnaddcl  8968  nnmulcl  8969  zaddcllempos  9319  zaddcllemneg  9321  nn0n0n1ge2b  9361  fzind  9397  fnn0ind  9398  uzaddcl  9615  elpq  9677  uzsubsubfz  10076  elfz1b  10119  elfz0ubfz0  10154  fz0fzdiffz0  10159  elfzmlbp  10161  fzofzim  10217  elfzom1elp1fzo  10231  elfzom1p1elfzo  10243  ssfzo12bi  10254  modfzo0difsn  10425  seq3val  10488  seqvalcd  10489  expcllem  10561  expap0  10580  apexp1  10729  faclbnd  10752  faclbnd6  10755  fihashf1rn  10799  omgadd  10813  hashfzp1  10835  seq3coll  10853  cjexp  10933  r19.29uz  11032  resqrexlemover  11050  resqrexlemlo  11053  resqrexlemcalc3  11056  absexp  11119  fimaxre2  11266  climshft  11343  climub  11383  climserle  11384  sumfct  11413  isumss2  11432  binom  11523  bcxmas  11528  clim2prod  11578  prodfap0  11584  prodfrecap  11585  prodfct  11626  demoivreALT  11812  dvdsdivcl  11887  dvdsfac  11897  oddnn02np1  11916  oddge22np1  11917  evennn02n  11918  evennn2n  11919  m1exp1  11937  nn0o  11943  flodddiv4  11970  gcdneg  12014  bezoutlemmain  12030  dfgcd2  12046  gcdmultiple  12052  nnwosdc  12071  alginv  12078  cncongr1  12134  prmdvdsexp  12179  prmndvdsfaclt  12187  dfgrp2  12968  srgmulgass  13340  lmodvsmmulgdi  13636  lmodfopnelem1  13637  rmodislmodlem  13663  cnfldmulg  13876  cnfldexp  13877  clsss  14070  xmettri2  14313  mettri  14325  metss  14446  zabsle1  14853  bdssexg  15109  bj-findis  15184  nninfalllem1  15211  nninfsellemdc  15213  redc0  15259