Theorem mpan 415

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpan.1	⊢ 𝜑
mpan.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpan	⊢ (𝜓 → 𝜒)

Proof of Theorem mpan

Step	Hyp	Ref	Expression
1		mpan.1	. . 3 ⊢ 𝜑
2	1	a1i 9	. 2 ⊢ (𝜓 → 𝜑)
3		mpan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpancom 413	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mp2an  417  mpanl12  427  mp3an1  1258  mp3an12  1261  mp3an13  1262  ax9o  1631  sbnfc2  2977  ssdifss  3119  undifss  3350  uneqdifeqim  3355  elssuni  3664  csbexa  3943  difexg  3955  rabexg  3957  abssexg  3991  snexg  3993  copsexg  4045  sotritric  4125  sotritrieq  4126  trsuc  4223  oneli  4229  unexb  4241  opeluu  4246  rabxfr  4266  reuhyp  4268  ordunisuc2r  4304  reg3exmid  4368  brrelexi  4450  brrelex2i  4451  xpss2  4517  opabid2  4535  eliunxp  4543  releldmi  4642  relelrni  4643  dmexg  4665  rnexg  4666  elres  4715  resexg  4719  relbrcnvg  4778  brcodir  4786  sotri  4794  sotri2  4796  sotri3  4797  dfrel2  4847  coi1  4912  fco  5140  fssres  5150  fabexg  5161  fvopab3g  5340  mpteqb  5356  ffvelrni  5396  fsn2  5434  dfmptg  5439  fvpr1  5462  fvconst2  5474  mptexg  5483  oprabid  5638  ovprc  5641  caovcl  5756  caovass  5762  caovdi  5781  elmpt2cl  5799  ofexg  5817  resfunexgALT  5838  fo1stresm  5889  fo2ndresm  5890  1stexg  5895  2ndexg  5896  elopabi  5922  mpt2exxg  5934  mpt2xopn0yelv  5958  rntpos  5976  smores  6011  tfr0dm  6041  tfrlemibxssdm  6046  tfrexlem  6053  tfr1onlembxssdm  6062  tfrcllembxssdm  6075  rdgruledefgg  6094  rdgruledefg  6095  rdgivallem  6100  rdgexg  6108  frec0g  6116  ordgt0ge1  6153  omfnex  6164  oeiv  6171  nna0r  6193  nnm0r  6194  nnsucsssuc  6207  nn2m  6237  nnaordex  6238  nnawordex  6239  ecdmn0m  6286  ecelqsi  6298  ecidg  6308  ectocl  6311  encv  6415  f1oen  6428  ssdomg  6447  map1  6481  fiprc  6484  xpdom1  6503  fict  6536  isinfinf  6565  ac6sfi  6566  xpfi  6590  en1eqsn  6606  eqinfti  6659  djueq2  6678  djulclr  6685  djurclr  6686  djulcl  6687  djurcl  6688  djuf1olem  6689  djulclb  6691  djuun  6704  eldju1st  6706  1stinl  6709  2ndinl  6710  1stinr  6711  2ndinr  6712  isomnimap  6737  0nnq  6867  mulidnq  6892  archnqq  6920  prarloclemarch2  6922  nqnq0pi  6941  nq0m0r  6959  nq02m  6968  prarloclemlt  6996  prarloclemn  7002  prarloclem5  7003  addnqprllem  7030  addnqprulem  7031  appdivnq  7066  1idprl  7093  1idpru  7094  addextpr  7124  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprlemnbj  7170  caucvgprlemloc  7178  caucvgprprlemnbj  7196  caucvgprprlemloc  7206  caucvgprprlemaddq  7211  0nsr  7239  ltsosr  7254  recexgt0sr  7263  prsrpos  7274  caucvgsr  7291  mulresr  7319  axcnre  7360  axpre-ltwlin  7362  mulid2  7430  0re  7432  axmulgt0  7502  ltnsym2  7519  eqlei  7522  ltnei  7532  muladd11  7559  cnegex  7604  0cnALT  7616  negcl  7626  negneg  7676  mul02  7809  mulm1  7822  lt0neg2  7891  le0neg2  7893  recexre  7996  recexgt0  7998  mulge0  8037  gt0ap0i  8044  recextlem1  8059  recexap  8061  recclapzi  8143  recap0apzi  8144  recidapzi  8145  divassapzi  8168  divmulapzi  8169  divdirapzi  8170  rerecclapzi  8182  ltp1  8240  recgt0i  8302  ltmul1i  8316  ltdiv1i  8317  ltmuldivi  8318  ltmul2i  8319  lemul1i  8320  lemul2i  8321  nngt1ne1  8391  nnrecre  8393  nn0ge0  8631  nn0addcl  8641  nn0mulcl  8642  zgt0ge1  8741  dfuzi  8789  eluzel2  8956  eluz2b1  9020  uz2m1nn  9024  nn01to3  9034  zq  9043  nnrecq  9062  rpge0  9078  rpreccl  9092  mnflt  9185  pnfnlt  9189  mnfle  9194  xrlelttr  9203  xrltletr  9204  xrletr  9205  xlt0neg2  9233  xle0neg2  9235  elioomnf  9318  ige3m2fz  9395  fzshftral  9452  ige2m1fz1  9453  1fv  9478  4fvwrd4  9479  rebtwn2zlemstep  9592  qbtwnxr  9597  btwnzge0  9635  zmodid2  9687  q2txmodxeq0  9719  frec2uzrand  9740  frecuzrdgtcl  9747  frecfzennn  9761  nn0ennn  9768  iseqeq4  9785  expival  9855  0exp  9888  sqgt0api  9938  subsq2  9959  bernneq  9970  faclbnd  10045  faclbnd2  10046  faclbnd3  10047  hashinfuni  10081  hashxp  10130  2shfti  10161  reim  10181  imcl  10183  crim  10187  caucvgre  10309  rennim  10330  resqrexlemdecn  10340  qabsor  10403  absimle  10412  sqrtthi  10447  sqrtcli  10448  sqrtgt0i  10449  sqrtmsqi  10450  sqrtsqi  10451  sqsqrti  10452  sqrtge0i  10453  absidi  10454  absnidi  10455  iserclim0  10586  0dvds  10691  odd2np1lem  10747  odd2np1  10748  even2n  10749  mod2eq0even  10753  2teven  10762  opoe  10770  omoe  10771  opeo  10772  omeo  10773  m1exp1  10776  gcd0id  10845  gcdid0  10846  1gcd  10858  lcmdvds  10936  isprm2lem  10973  isprm3  10975  prmgt1  10988  coprm  10998  isevengcd2  11012  isoddgcd1  11013  sqpweven  11028  2sqpwodd  11029  unennn  11085  djucllem  11138  bdrabexg  11235  bdunexb  11249  peano5set  11273  speano5  11277  bj-omtrans  11289  nninfsellemeq  11344