Theorem impcom 124

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 123	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  mpan9  277  19.41h  1644  19.41  1645  equtr2  1668  mopick  2051  2euex  2060  gencl  2687  2gencl  2688  rspccva  2757  indifdir  3296  sseq0  3368  minel  3388  r19.2m  3413  r19.2mOLD  3414  elelpwi  3486  ssuni  3722  disjiun  3888  trintssm  4000  ssexg  4025  pofun  4192  sowlin  4200  2optocl  4574  3optocl  4575  elrnmpt1  4748  resieq  4785  fnun  5185  fss  5240  fun  5251  dmfex  5268  fvelimab  5429  mptfvex  5458  fmptco  5538  fnressn  5558  fressnfv  5559  fvtp2g  5581  fvtp3g  5582  fnex  5594  funfvima3  5603  isores3  5668  f1o2ndf1  6077  reldmtpos  6102  smores  6141  tfrlem7  6166  tfrlemi1  6181  tfrexlem  6183  tfrcl  6213  frecrdg  6257  nnacl  6328  nnmcl  6329  nnmsucr  6336  nntri3or  6341  nnaword  6359  nnaordex  6375  2ecoptocl  6469  ssct  6663  enm  6665  xpf1o  6689  ac6sfi  6743  f1dmvrnfibi  6782  f1vrnfibi  6783  updjud  6917  enumct  6950  elni2  7064  ax1rid  7606  negf1o  8057  mulgt1  8525  lbreu  8607  nnaddcl  8644  nnmulcl  8645  zaddcllempos  8989  zaddcllemneg  8991  nn0n0n1ge2b  9028  fzind  9064  fnn0ind  9065  uzaddcl  9277  uzsubsubfz  9714  elfz1b  9757  elfz0ubfz0  9789  fz0fzdiffz0  9794  elfzmlbp  9796  fzofzim  9852  elfzom1elp1fzo  9866  elfzom1p1elfzo  9878  ssfzo12bi  9889  modfzo0difsn  10055  seq3val  10118  seqvalcd  10119  expcllem  10191  expap0  10210  faclbnd  10374  faclbnd6  10377  fihashf1rn  10422  omgadd  10435  hashfzp1  10457  seq3coll  10472  cjexp  10552  r19.29uz  10650  resqrexlemover  10668  resqrexlemlo  10671  resqrexlemcalc3  10674  absexp  10737  fimaxre2  10884  climshft  10959  climub  10999  climserle  11000  sumfct  11029  isumss2  11048  binom  11139  bcxmas  11144  demoivreALT  11324  dvdsdivcl  11390  dvdsfac  11400  oddnn02np1  11419  oddge22np1  11420  evennn02n  11421  evennn2n  11422  m1exp1  11440  nn0o  11446  flodddiv4  11473  gcdneg  11512  bezoutlemmain  11526  dfgcd2  11542  gcdmultiple  11548  alginv  11568  cncongr1  11624  prmdvdsexp  11666  prmndvdsfaclt  11674  clsss  12124  xmettri2  12344  mettri  12356  metss  12477  bdssexg  12785  bj-findis  12860  nninfalllemn  12883  nninfalllem1  12884  nninfsellemdc  12887