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  1618  19.41  1619  equtr2  1641  mopick  2023  2euex  2032  gencl  2645  2gencl  2646  rspccva  2714  indifdir  3244  sseq0  3312  minel  3332  r19.2m  3356  elelpwi  3426  ssuni  3660  trintssm  3929  ssexg  3955  pofun  4115  sowlin  4123  2optocl  4485  3optocl  4486  elrnmpt1  4656  resieq  4693  fnun  5087  fss  5138  fun  5149  dmfex  5165  fvelimab  5325  mptfvex  5353  fmptco  5429  fnressn  5448  fressnfv  5449  fvtp2g  5469  fvtp3g  5470  fnex  5482  funfvima3  5491  isores3  5557  f1o2ndf1  5952  reldmtpos  5974  smores  6013  tfrlem7  6038  tfrlemi1  6053  tfrexlem  6055  tfrcl  6085  frecrdg  6129  nnacl  6197  nnmcl  6198  nnmsucr  6205  nntri3or  6210  nnaword  6224  nnaordex  6240  2ecoptocl  6334  ssct  6488  enm  6490  xpf1o  6514  ac6sfi  6568  f1dmvrnfibi  6606  f1vrnfibi  6607  updjud  6720  elni2  6820  ax1rid  7359  negf1o  7807  mulgt1  8262  lbreu  8344  nnaddcl  8380  nnmulcl  8381  zaddcllempos  8723  zaddcllemneg  8725  nn0n0n1ge2b  8762  fzind  8797  fnn0ind  8798  uzaddcl  9009  uzsubsubfz  9396  elfz1b  9437  elfz0ubfz0  9467  fz0fzdiffz0  9472  elfzmlbp  9474  fzofzim  9530  elfzom1elp1fzo  9544  elfzom1p1elfzo  9556  ssfzo12bi  9567  modfzo0difsn  9733  iseqvalt  9793  iseqoveq  9802  iseqss  9803  iseqsst  9804  expivallem  9858  expcllem  9868  expap0  9887  faclbnd  10049  faclbnd6  10052  fihashf1rn  10097  omgadd  10110  hashfzp1  10132  iseqcoll  10147  cjexp  10226  r19.29uz  10324  resqrexlemover  10342  resqrexlemlo  10345  resqrexlemcalc3  10348  absexp  10411  fimaxre2  10556  climshft  10590  climub  10629  climserile  10630  sumfct  10658  isumss2  10676  dvdsdivcl  10757  dvdsfac  10767  oddnn02np1  10786  oddge22np1  10787  evennn02n  10788  evennn2n  10789  m1exp1  10807  nn0o  10813  flodddiv4  10840  gcdneg  10879  bezoutlemmain  10893  dfgcd2  10909  gcdmultiple  10915  ialginv  10935  cncongr1  10991  prmdvdsexp  11033  prmndvdsfaclt  11041  bdssexg  11264  bj-findis  11343  nninfalllemn  11367  nninfalllem1  11368  nninfsellemdc  11371