Theorem mpan 424

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 422	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mp2an  426  mpanl12  436  mp3an1  1335  mp3an12  1338  mp3an13  1339  ax9o  1712  sbnfc2  3145  ssdifss  3294  undifss  3532  uneqdifeqim  3537  elssuni  3868  csbexa  4163  difexg  4175  rabexg  4177  abssexg  4216  snexg  4218  copsexg  4278  sotritric  4360  sotritrieq  4361  trsuc  4458  oneli  4464  unexb  4478  opeluu  4486  rabxfr  4506  reuhyp  4508  ordunisuc2r  4551  reg3exmid  4617  brrelex12i  4706  brrelex1i  4707  brrelex2i  4708  xpss2  4775  opabid2  4798  eliunxp  4806  releldmi  4906  relelrni  4907  dmexg  4931  rnexg  4932  elres  4983  resexg  4987  relbrcnvg  5049  brcodir  5058  sotri  5066  sotri2  5068  sotri3  5069  dfrel2  5121  coi1  5186  fco  5426  fssres  5436  fabexg  5448  fvopab3g  5637  mptrcl  5647  mpteqb  5655  elfvmptrab1  5659  ffvelcdmi  5699  fsn2  5739  dfmptg  5744  fvpr1  5769  fvconst2  5781  mptexg  5790  oprabid  5957  ovprc  5961  caovcl  6082  caovass  6088  caovdi  6107  elmpocl  6122  ofexg  6144  resfunexgALT  6174  fo1stresm  6228  fo2ndresm  6229  1stexg  6234  2ndexg  6235  elopabi  6262  mpoexxg  6277  mpoxopn0yelv  6306  rntpos  6324  smores  6359  tfr0dm  6389  tfrlemibxssdm  6394  tfrexlem  6401  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  rdgruledefgg  6442  rdgruledefg  6443  rdgivallem  6448  rdgexg  6456  frec0g  6464  ordgt0ge1  6502  omfnex  6516  oeiv  6523  nna0r  6545  nnm0r  6546  nnsucsssuc  6559  nn2m  6594  nnaordex  6595  nnawordex  6596  ecdmn0m  6645  ecelqsi  6657  ecidg  6667  ectocl  6670  encv  6814  f1oen  6827  ssdomg  6846  map1  6880  fiprc  6883  xpdom1  6903  fict  6938  isinfinf  6967  ac6sfi  6968  xpfi  7002  en1eqsn  7023  fidcenumlemr  7030  fiss  7052  eqinfti  7095  djueq2  7116  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djuf1olem  7128  djulclb  7130  inl11  7140  eldju1st  7146  1stinl  7149  2ndinl  7150  1stinr  7151  2ndinr  7152  ctssdccl  7186  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  finacn  7289  djucomen  7301  exmidapne  7345  0nnq  7450  mulidnq  7475  archnqq  7503  prarloclemarch2  7505  nqnq0pi  7524  nq0m0r  7542  nq02m  7551  prarloclemlt  7579  prarloclemn  7585  prarloclem5  7586  addnqprllem  7613  addnqprulem  7614  appdivnq  7649  1idprl  7676  1idpru  7677  addextpr  7707  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemnbj  7753  caucvgprlemloc  7761  caucvgprprlemnbj  7779  caucvgprprlemloc  7789  caucvgprprlemaddq  7794  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemloc  7807  suplocexprlemlub  7810  0nsr  7835  ltsosr  7850  recexgt0sr  7859  prsrpos  7871  caucvgsr  7888  mappsrprg  7890  suplocsrlem  7894  mulresr  7924  axcnre  7967  axpre-ltwlin  7969  mullid  8043  0re  8045  axmulgt0  8117  ltnsym2  8136  eqlei  8139  ltnei  8149  muladd11  8178  cnegex  8223  0cnALT  8235  negcl  8245  negneg  8295  mul02  8432  mulm1  8445  lt0neg2  8515  le0neg2  8517  recexre  8624  recexgt0  8626  mulge0  8665  gt0ap0i  8673  recextlem1  8697  recexap  8699  recclapzi  8783  recap0apzi  8784  recidapzi  8785  divassapzi  8808  divmulapzi  8809  divdirapzi  8810  rerecclapzi  8822  ltp1  8890  recgt0i  8952  ltmul1i  8966  ltdiv1i  8967  ltmuldivi  8968  ltmul2i  8969  lemul1i  8970  lemul2i  8971  sup3exmid  9003  nngt1ne1  9044  nnrecre  9046  nn0ge0  9293  nn0addcl  9303  nn0mulcl  9304  zgt0ge1  9403  dfuzi  9455  eluzel2  9625  eluz2b1  9694  uz2m1nn  9698  elnn0dc  9704  elnndc  9705  nn01to3  9710  zq  9719  nnrecq  9738  rpge0  9760  rpreccl  9774  mnflt  9877  pnfnlt  9881  mnfle  9886  xrlelttr  9900  xrltletr  9901  xrletr  9902  xgepnf  9910  xlt0neg2  9933  xle0neg2  9935  xaddpnf2  9941  xaddmnf2  9943  xaddid2  9957  elioomnf  10062  ige3m2fz  10143  fzshftral  10202  ige2m1fz1  10203  1fv  10233  4fvwrd4  10234  rebtwn2zlemstep  10361  qbtwnxr  10366  btwnzge0  10409  zmodid2  10463  q2txmodxeq0  10495  frec2uzrand  10516  frecuzrdgtcl  10523  frecfzennn  10537  nn0ennn  10544  uzennn  10547  0exp  10685  sqgt0api  10736  subsq2  10758  qsqeqor  10761  bernneq  10771  faclbnd  10852  faclbnd2  10853  faclbnd3  10854  hashinfuni  10888  hashxp  10937  iswrdiz  10961  2shfti  11015  reim  11036  imcl  11038  crim  11042  caucvgre  11165  rennim  11186  resqrexlemdecn  11196  qabsor  11259  absimle  11268  sqrtthi  11303  sqrtcli  11304  sqrtgt0i  11305  sqrtmsqi  11306  sqrtsqi  11307  sqsqrti  11308  sqrtge0i  11309  absidi  11310  absnidi  11311  xrmaxiflemlub  11432  serclim0  11489  fsum2d  11619  fsumcnv  11621  fsumconst  11638  modfsummodlem1  11640  fsumabs  11649  binom11  11670  prodf1  11726  prodfclim1  11728  prodsnf  11776  fprod2d  11807  fprodcnv  11809  efzval  11867  eftlub  11874  efsep  11875  ef4p  11878  efgt1  11881  reef11  11883  sinf  11888  cosf  11889  efi4p  11901  sinneg  11910  cosneg  11911  efival  11916  efmival  11917  cos01gt0  11947  sin02gt0  11948  absefib  11955  efieq1re  11956  demoivre  11957  demoivreALT  11958  eirraplem  11961  0dvds  11995  odd2np1lem  12056  odd2np1  12057  even2n  12058  mod2eq0even  12062  2teven  12071  opoe  12079  omoe  12080  opeo  12081  omeo  12082  m1exp1  12085  bits0e  12133  bits0o  12134  bitsinv1  12146  gcd0id  12173  gcdid0  12174  1gcd  12186  lcmdvds  12274  isprm2lem  12311  isprm3  12313  prmgt1  12327  coprm  12339  isevengcd2  12353  isoddgcd1  12354  sqpweven  12370  2sqpwodd  12371  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pythagtriplem16  12475  pc2dvds  12526  oddprmdvds  12550  pockthi  12554  1arith2  12564  unennn  12641  ctinfomlemom  12671  qnnen  12675  ssnnctlemct  12690  strslfv  12750  strle1g  12811  1strbas  12822  tgval  12966  ismgmn0  13062  mulgval  13330  mulgfng  13332  mulg0  13333  mulg1  13337  mulg2  13339  isnsg  13410  ringidvalg  13595  issrg  13599  subrgpropd  13887  rrgval  13896  islmod  13925  scaffvalg  13940  islssm  13991  sraval  14071  mopnset  14186  metuex  14189  zrhval  14251  zrhvalg  14252  zrhex  14255  psrbag  14301  istopon  14335  eltg4i  14377  eltg3  14379  tg1  14381  tg2  14382  topnex  14408  cldrcl  14424  restsn  14502  lmrcl  14513  metflem  14671  xmetf  14672  ismet2  14676  xmeteq0  14681  xmettri2  14683  xmetpsmet  14691  xmetres2  14701  blfvalps  14707  blex  14709  blvalps  14710  blval  14711  blfps  14731  blf  14732  mopnval  14764  cnbl0  14856  cnblcld  14857  blssioo  14875  resubmet  14878  cncfmet  14914  cnplimcim  14989  cnlimcim  14993  cnlimc  14994  dvfgg  15010  dvfpm  15011  dvfcnpm  15012  dvcj  15031  dvmptfsum  15047  reeff1olem  15093  ef2kpi  15128  sinperlem  15130  sin2kpi  15133  cos2kpi  15134  sinhalfpip  15142  sinhalfpim  15143  coshalfpip  15144  coshalfpim  15145  sincosq1sgn  15148  sinq12gt0  15152  sinkpi  15169  reeflog  15185  relogef  15186  logrpap0b  15198  loggt0b  15213  1cxp  15222  ecxp  15223  2logb9irrap  15299  0sgm  15307  lgsval2lem  15337  m1lgs  15412  djucllem  15532  bdrabexg  15638  bdunexb  15652  peano5set  15672  speano5  15676  bj-omtrans  15688  pwf1oexmid  15732  nninfsellemeq  15747  iswomninnlem  15784