Theorem impcom 123

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mpan9  275  19.41h  1615  19.41  1616  equtr2  1637  mopick  2019  2euex  2028  gencl  2631  2gencl  2632  rspccva  2700  indifdir  3220  sseq0  3285  minel  3305  r19.2m  3329  elelpwi  3393  ssuni  3623  trintssm  3891  ssexg  3917  pofun  4067  sowlin  4075  2optocl  4435  3optocl  4436  elrnmpt1  4603  resieq  4640  fnun  5025  fss  5074  fun  5083  dmfex  5099  fvelimab  5250  mptfvex  5277  fmptco  5351  fnressn  5370  fressnfv  5371  fvtp2g  5391  fvtp3g  5392  fnex  5404  funfvima3  5413  isores3  5475  f1o2ndf1  5869  reldmtpos  5891  smores  5930  tfrlem7  5956  tfrlemi1  5969  tfrexlem  5971  rdgon  5996  frecrdg  6015  nnacl  6082  nnmcl  6083  nnmsucr  6090  nntri3or  6095  nnaword  6107  nnaordex  6123  2ecoptocl  6217  enm  6317  ac6sfi  6379  f1dmvrnfibi  6393  f1vrnfibi  6394  elni2  6504  ax1rid  7043  negf1o  7486  mulgt1  7941  lbreu  8023  nnaddcl  8059  nnmulcl  8060  zaddcllempos  8388  zaddcllemneg  8390  nn0n0n1ge2b  8427  fzind  8462  fnn0ind  8463  uzaddcl  8674  uzsubsubfz  9066  elfz1b  9107  elfz0ubfz0  9136  fz0fzdiffz0  9141  elfzmlbp  9143  fzofzim  9197  elfzom1elp1fzo  9211  elfzom1p1elfzo  9223  ssfzo12bi  9234  modfzo0difsn  9397  iseqss  9446  expivallem  9477  expcllem  9487  expap0  9506  faclbnd  9668  faclbnd6  9671  cjexp  9780  r19.29uz  9878  resqrexlemover  9896  resqrexlemlo  9899  resqrexlemcalc3  9902  absexp  9965  fimaxre2  10109  climshft  10143  climub  10182  climserile  10183  dvdsdivcl  10250  dvdsfac  10260  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283  m1exp1  10301  nn0o  10307  flodddiv4  10334  gcdneg  10373  bezoutlemmain  10387  dfgcd2  10403  gcdmultiple  10409  ialginv  10429  cncongr1  10485  prmdvdsexp  10527  prmndvdsfaclt  10535  bdssexg  10695  bj-findis  10774