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  1707  19.41  1708  equtr2  1733  mopick  2131  2euex  2140  gencl  2803  2gencl  2804  rspccva  2875  indifdir  3428  sseq0  3501  minel  3521  r19.2m  3546  r19.2mOLD  3547  elelpwi  3627  ssuni  3871  disjiun  4038  trintssm  4157  ssexg  4182  pofun  4358  sowlin  4366  2optocl  4751  3optocl  4752  elrnmpt1  4928  resieq  4968  fnun  5381  fss  5436  fun  5447  dmfex  5464  fvelimab  5634  mptfvex  5664  fmptco  5745  fnressn  5769  fressnfv  5770  fvtp2g  5792  fvtp3g  5793  fnex  5805  funfvima3  5817  isores3  5883  f1o2ndf1  6313  reldmtpos  6338  smores  6377  tfrlem7  6402  tfrlemi1  6417  tfrexlem  6419  tfrcl  6449  frecrdg  6493  nnacl  6565  nnmcl  6566  nnmsucr  6573  nntri3or  6578  nnaword  6596  nnaordex  6613  2ecoptocl  6709  ssct  6912  enm  6914  xpf1o  6940  ac6sfi  6994  f1dmvrnfibi  7045  f1vrnfibi  7046  updjud  7183  enumct  7216  nnnninfeq  7229  exmidontriimlem4  7335  exmidontriim  7336  elni2  7426  ax1rid  7989  negf1o  8453  mulgt1  8935  lbreu  9017  nnaddcl  9055  nnmulcl  9056  zaddcllempos  9408  zaddcllemneg  9410  nn0n0n1ge2b  9451  fzind  9487  fnn0ind  9488  uzaddcl  9706  elpq  9769  uzsubsubfz  10168  elfz1b  10211  elfz0ubfz0  10246  fz0fzdiffz0  10251  elfzmlbp  10253  fzofzim  10310  elfzom1elp1fzo  10329  elfzom1p1elfzo  10341  ssfzo12bi  10352  modfzo0difsn  10538  seq3val  10603  seqvalcd  10604  expcllem  10693  expap0  10712  apexp1  10861  faclbnd  10884  faclbnd6  10887  fihashf1rn  10931  omgadd  10945  hashfzp1  10967  seq3coll  10985  fundm2domnop0  10988  lswlgt0cl  11043  ccatsymb  11056  cjexp  11146  r19.29uz  11245  resqrexlemover  11263  resqrexlemlo  11266  resqrexlemcalc3  11269  absexp  11332  fimaxre2  11480  climshft  11557  climub  11597  climserle  11598  sumfct  11627  isumss2  11646  binom  11737  bcxmas  11742  clim2prod  11792  prodfap0  11798  prodfrecap  11799  prodfct  11840  demoivreALT  12027  dvdsdivcl  12103  dvdsfac  12113  oddnn02np1  12133  oddge22np1  12134  evennn02n  12135  evennn2n  12136  m1exp1  12154  nn0o  12160  flodddiv4  12189  gcdneg  12245  bezoutlemmain  12261  dfgcd2  12277  gcdmultiple  12283  nnwosdc  12302  alginv  12311  cncongr1  12367  prmdvdsexp  12412  prmndvdsfaclt  12420  dfgrp2  13301  srgmulgass  13693  lmodvsmmulgdi  14027  lmodfopnelem1  14028  rmodislmodlem  14054  cnfldmulg  14280  cnfldexp  14281  clsss  14532  xmettri2  14775  mettri  14787  metss  14908  plycolemc  15172  zabsle1  15418  gausslemma2dlem1a  15477  gausslemma2dlem2  15481  gausslemma2dlem3  15482  gausslemma2dlem4  15483  2lgslem1a1  15505  bdssexg  15773  bj-findis  15848  nninfalllem1  15878  nninfsellemdc  15880  redc0  15929