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  3420  sseq0  3493  minel  3513  r19.2m  3538  r19.2mOLD  3539  elelpwi  3618  ssuni  3862  disjiun  4029  trintssm  4148  ssexg  4173  pofun  4348  sowlin  4356  2optocl  4741  3optocl  4742  elrnmpt1  4918  resieq  4957  fnun  5367  fss  5422  fun  5433  dmfex  5450  fvelimab  5620  mptfvex  5650  fmptco  5731  fnressn  5751  fressnfv  5752  fvtp2g  5774  fvtp3g  5775  fnex  5787  funfvima3  5799  isores3  5865  f1o2ndf1  6295  reldmtpos  6320  smores  6359  tfrlem7  6384  tfrlemi1  6399  tfrexlem  6401  tfrcl  6431  frecrdg  6475  nnacl  6547  nnmcl  6548  nnmsucr  6555  nntri3or  6560  nnaword  6578  nnaordex  6595  2ecoptocl  6691  ssct  6886  enm  6888  xpf1o  6914  ac6sfi  6968  f1dmvrnfibi  7019  f1vrnfibi  7020  updjud  7157  enumct  7190  nnnninfeq  7203  exmidontriimlem4  7309  exmidontriim  7310  elni2  7400  ax1rid  7963  negf1o  8427  mulgt1  8909  lbreu  8991  nnaddcl  9029  nnmulcl  9030  zaddcllempos  9382  zaddcllemneg  9384  nn0n0n1ge2b  9424  fzind  9460  fnn0ind  9461  uzaddcl  9679  elpq  9742  uzsubsubfz  10141  elfz1b  10184  elfz0ubfz0  10219  fz0fzdiffz0  10224  elfzmlbp  10226  fzofzim  10283  elfzom1elp1fzo  10297  elfzom1p1elfzo  10309  ssfzo12bi  10320  modfzo0difsn  10506  seq3val  10571  seqvalcd  10572  expcllem  10661  expap0  10680  apexp1  10829  faclbnd  10852  faclbnd6  10855  fihashf1rn  10899  omgadd  10913  hashfzp1  10935  seq3coll  10953  cjexp  11077  r19.29uz  11176  resqrexlemover  11194  resqrexlemlo  11197  resqrexlemcalc3  11200  absexp  11263  fimaxre2  11411  climshft  11488  climub  11528  climserle  11529  sumfct  11558  isumss2  11577  binom  11668  bcxmas  11673  clim2prod  11723  prodfap0  11729  prodfrecap  11730  prodfct  11771  demoivreALT  11958  dvdsdivcl  12034  dvdsfac  12044  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  m1exp1  12085  nn0o  12091  flodddiv4  12120  gcdneg  12176  bezoutlemmain  12192  dfgcd2  12208  gcdmultiple  12214  nnwosdc  12233  alginv  12242  cncongr1  12298  prmdvdsexp  12343  prmndvdsfaclt  12351  dfgrp2  13231  srgmulgass  13623  lmodvsmmulgdi  13957  lmodfopnelem1  13958  rmodislmodlem  13984  cnfldmulg  14210  cnfldexp  14211  clsss  14462  xmettri2  14705  mettri  14717  metss  14838  plycolemc  15102  zabsle1  15348  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  gausslemma2dlem3  15412  gausslemma2dlem4  15413  2lgslem1a1  15435  bdssexg  15658  bj-findis  15733  nninfalllem1  15763  nninfsellemdc  15765  redc0  15814