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  1685  19.41  1686  equtr2  1711  mopick  2104  2euex  2113  gencl  2769  2gencl  2770  rspccva  2840  indifdir  3391  sseq0  3464  minel  3484  r19.2m  3509  r19.2mOLD  3510  elelpwi  3587  ssuni  3830  disjiun  3996  trintssm  4115  ssexg  4140  pofun  4310  sowlin  4318  2optocl  4701  3optocl  4702  elrnmpt1  4875  resieq  4914  fnun  5319  fss  5374  fun  5385  dmfex  5402  fvelimab  5569  mptfvex  5598  fmptco  5679  fnressn  5699  fressnfv  5700  fvtp2g  5722  fvtp3g  5723  fnex  5735  funfvima3  5746  isores3  5811  f1o2ndf1  6224  reldmtpos  6249  smores  6288  tfrlem7  6313  tfrlemi1  6328  tfrexlem  6330  tfrcl  6360  frecrdg  6404  nnacl  6476  nnmcl  6477  nnmsucr  6484  nntri3or  6489  nnaword  6507  nnaordex  6524  2ecoptocl  6618  ssct  6813  enm  6815  xpf1o  6839  ac6sfi  6893  f1dmvrnfibi  6938  f1vrnfibi  6939  updjud  7076  enumct  7109  nnnninfeq  7121  exmidontriimlem4  7218  exmidontriim  7219  elni2  7308  ax1rid  7871  negf1o  8333  mulgt1  8814  lbreu  8896  nnaddcl  8933  nnmulcl  8934  zaddcllempos  9284  zaddcllemneg  9286  nn0n0n1ge2b  9326  fzind  9362  fnn0ind  9363  uzaddcl  9580  elpq  9642  uzsubsubfz  10040  elfz1b  10083  elfz0ubfz0  10118  fz0fzdiffz0  10123  elfzmlbp  10125  fzofzim  10181  elfzom1elp1fzo  10195  elfzom1p1elfzo  10207  ssfzo12bi  10218  modfzo0difsn  10388  seq3val  10451  seqvalcd  10452  expcllem  10524  expap0  10543  apexp1  10689  faclbnd  10712  faclbnd6  10715  fihashf1rn  10759  omgadd  10773  hashfzp1  10795  seq3coll  10813  cjexp  10893  r19.29uz  10992  resqrexlemover  11010  resqrexlemlo  11013  resqrexlemcalc3  11016  absexp  11079  fimaxre2  11226  climshft  11303  climub  11343  climserle  11344  sumfct  11373  isumss2  11392  binom  11483  bcxmas  11488  clim2prod  11538  prodfap0  11544  prodfrecap  11545  prodfct  11586  demoivreALT  11772  dvdsdivcl  11846  dvdsfac  11856  oddnn02np1  11875  oddge22np1  11876  evennn02n  11877  evennn2n  11878  m1exp1  11896  nn0o  11902  flodddiv4  11929  gcdneg  11973  bezoutlemmain  11989  dfgcd2  12005  gcdmultiple  12011  nnwosdc  12030  alginv  12037  cncongr1  12093  prmdvdsexp  12138  prmndvdsfaclt  12146  dfgrp2  12830  srgmulgass  13072  cnfldmulg  13275  cnfldexp  13276  clsss  13400  xmettri2  13643  mettri  13655  metss  13776  zabsle1  14182  bdssexg  14427  bj-findis  14502  nninfalllem1  14528  nninfsellemdc  14530  redc0  14576