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  1683  19.41  1684  equtr2  1709  mopick  2102  2euex  2111  gencl  2767  2gencl  2768  rspccva  2838  indifdir  3389  sseq0  3462  minel  3482  r19.2m  3507  r19.2mOLD  3508  elelpwi  3584  ssuni  3827  disjiun  3993  trintssm  4112  ssexg  4137  pofun  4306  sowlin  4314  2optocl  4697  3optocl  4698  elrnmpt1  4871  resieq  4910  fnun  5314  fss  5369  fun  5380  dmfex  5397  fvelimab  5564  mptfvex  5593  fmptco  5674  fnressn  5694  fressnfv  5695  fvtp2g  5717  fvtp3g  5718  fnex  5730  funfvima3  5741  isores3  5806  f1o2ndf1  6219  reldmtpos  6244  smores  6283  tfrlem7  6308  tfrlemi1  6323  tfrexlem  6325  tfrcl  6355  frecrdg  6399  nnacl  6471  nnmcl  6472  nnmsucr  6479  nntri3or  6484  nnaword  6502  nnaordex  6519  2ecoptocl  6613  ssct  6808  enm  6810  xpf1o  6834  ac6sfi  6888  f1dmvrnfibi  6933  f1vrnfibi  6934  updjud  7071  enumct  7104  nnnninfeq  7116  exmidontriimlem4  7213  exmidontriim  7214  elni2  7288  ax1rid  7851  negf1o  8313  mulgt1  8791  lbreu  8873  nnaddcl  8910  nnmulcl  8911  zaddcllempos  9261  zaddcllemneg  9263  nn0n0n1ge2b  9303  fzind  9339  fnn0ind  9340  uzaddcl  9557  elpq  9619  uzsubsubfz  10015  elfz1b  10058  elfz0ubfz0  10093  fz0fzdiffz0  10098  elfzmlbp  10100  fzofzim  10156  elfzom1elp1fzo  10170  elfzom1p1elfzo  10182  ssfzo12bi  10193  modfzo0difsn  10363  seq3val  10426  seqvalcd  10427  expcllem  10499  expap0  10518  apexp1  10664  faclbnd  10687  faclbnd6  10690  fihashf1rn  10734  omgadd  10748  hashfzp1  10770  seq3coll  10788  cjexp  10868  r19.29uz  10967  resqrexlemover  10985  resqrexlemlo  10988  resqrexlemcalc3  10991  absexp  11054  fimaxre2  11201  climshft  11278  climub  11318  climserle  11319  sumfct  11348  isumss2  11367  binom  11458  bcxmas  11463  clim2prod  11513  prodfap0  11519  prodfrecap  11520  prodfct  11561  demoivreALT  11747  dvdsdivcl  11821  dvdsfac  11831  oddnn02np1  11850  oddge22np1  11851  evennn02n  11852  evennn2n  11853  m1exp1  11871  nn0o  11877  flodddiv4  11904  gcdneg  11948  bezoutlemmain  11964  dfgcd2  11980  gcdmultiple  11986  nnwosdc  12005  alginv  12012  cncongr1  12068  prmdvdsexp  12113  prmndvdsfaclt  12121  dfgrp2  12762  srgmulgass  12965  clsss  13169  xmettri2  13412  mettri  13424  metss  13545  zabsle1  13951  bdssexg  14196  bj-findis  14271  nninfalllem1  14298  nninfsellemdc  14300  redc0  14346