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  1709  sbnfc2  3141  ssdifss  3289  undifss  3527  uneqdifeqim  3532  elssuni  3863  csbexa  4158  difexg  4170  rabexg  4172  abssexg  4211  snexg  4213  copsexg  4273  sotritric  4355  sotritrieq  4356  trsuc  4453  oneli  4459  unexb  4473  opeluu  4481  rabxfr  4501  reuhyp  4503  ordunisuc2r  4546  reg3exmid  4612  brrelex12i  4701  brrelex1i  4702  brrelex2i  4703  xpss2  4770  opabid2  4793  eliunxp  4801  releldmi  4901  relelrni  4902  dmexg  4926  rnexg  4927  elres  4978  resexg  4982  relbrcnvg  5044  brcodir  5053  sotri  5061  sotri2  5063  sotri3  5064  dfrel2  5116  coi1  5181  fco  5419  fssres  5429  fabexg  5441  fvopab3g  5630  mptrcl  5640  mpteqb  5648  elfvmptrab1  5652  ffvelcdmi  5692  fsn2  5732  dfmptg  5737  fvpr1  5762  fvconst2  5774  mptexg  5783  oprabid  5950  ovprc  5953  caovcl  6073  caovass  6079  caovdi  6098  elmpocl  6113  ofexg  6135  resfunexgALT  6160  fo1stresm  6214  fo2ndresm  6215  1stexg  6220  2ndexg  6221  elopabi  6248  mpoexxg  6263  mpoxopn0yelv  6292  rntpos  6310  smores  6345  tfr0dm  6375  tfrlemibxssdm  6380  tfrexlem  6387  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  rdgruledefgg  6428  rdgruledefg  6429  rdgivallem  6434  rdgexg  6442  frec0g  6450  ordgt0ge1  6488  omfnex  6502  oeiv  6509  nna0r  6531  nnm0r  6532  nnsucsssuc  6545  nn2m  6580  nnaordex  6581  nnawordex  6582  ecdmn0m  6631  ecelqsi  6643  ecidg  6653  ectocl  6656  encv  6800  f1oen  6813  ssdomg  6832  map1  6866  fiprc  6869  xpdom1  6889  fict  6924  isinfinf  6953  ac6sfi  6954  xpfi  6986  en1eqsn  7007  fidcenumlemr  7014  fiss  7036  eqinfti  7079  djueq2  7100  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  djuf1olem  7112  djulclb  7114  inl11  7124  eldju1st  7130  1stinl  7133  2ndinl  7134  1stinr  7135  2ndinr  7136  ctssdccl  7170  isomnimap  7196  ismkvmap  7213  iswomnimap  7225  djucomen  7276  exmidapne  7320  0nnq  7424  mulidnq  7449  archnqq  7477  prarloclemarch2  7479  nqnq0pi  7498  nq0m0r  7516  nq02m  7525  prarloclemlt  7553  prarloclemn  7559  prarloclem5  7560  addnqprllem  7587  addnqprulem  7588  appdivnq  7623  1idprl  7650  1idpru  7651  addextpr  7681  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemnbj  7727  caucvgprlemloc  7735  caucvgprprlemnbj  7753  caucvgprprlemloc  7763  caucvgprprlemaddq  7768  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemloc  7781  suplocexprlemlub  7784  0nsr  7809  ltsosr  7824  recexgt0sr  7833  prsrpos  7845  caucvgsr  7862  mappsrprg  7864  suplocsrlem  7868  mulresr  7898  axcnre  7941  axpre-ltwlin  7943  mullid  8017  0re  8019  axmulgt0  8091  ltnsym2  8110  eqlei  8113  ltnei  8123  muladd11  8152  cnegex  8197  0cnALT  8209  negcl  8219  negneg  8269  mul02  8406  mulm1  8419  lt0neg2  8488  le0neg2  8490  recexre  8597  recexgt0  8599  mulge0  8638  gt0ap0i  8646  recextlem1  8670  recexap  8672  recclapzi  8756  recap0apzi  8757  recidapzi  8758  divassapzi  8781  divmulapzi  8782  divdirapzi  8783  rerecclapzi  8795  ltp1  8863  recgt0i  8925  ltmul1i  8939  ltdiv1i  8940  ltmuldivi  8941  ltmul2i  8942  lemul1i  8943  lemul2i  8944  sup3exmid  8976  nngt1ne1  9017  nnrecre  9019  nn0ge0  9265  nn0addcl  9275  nn0mulcl  9276  zgt0ge1  9375  dfuzi  9427  eluzel2  9597  eluz2b1  9666  uz2m1nn  9670  elnn0dc  9676  elnndc  9677  nn01to3  9682  zq  9691  nnrecq  9710  rpge0  9732  rpreccl  9746  mnflt  9849  pnfnlt  9853  mnfle  9858  xrlelttr  9872  xrltletr  9873  xrletr  9874  xgepnf  9882  xlt0neg2  9905  xle0neg2  9907  xaddpnf2  9913  xaddmnf2  9915  xaddid2  9929  elioomnf  10034  ige3m2fz  10115  fzshftral  10174  ige2m1fz1  10175  1fv  10205  4fvwrd4  10206  rebtwn2zlemstep  10321  qbtwnxr  10326  btwnzge0  10369  zmodid2  10423  q2txmodxeq0  10455  frec2uzrand  10476  frecuzrdgtcl  10483  frecfzennn  10497  nn0ennn  10504  uzennn  10507  0exp  10645  sqgt0api  10696  subsq2  10718  qsqeqor  10721  bernneq  10731  faclbnd  10812  faclbnd2  10813  faclbnd3  10814  hashinfuni  10848  hashxp  10897  iswrdiz  10921  2shfti  10975  reim  10996  imcl  10998  crim  11002  caucvgre  11125  rennim  11146  resqrexlemdecn  11156  qabsor  11219  absimle  11228  sqrtthi  11263  sqrtcli  11264  sqrtgt0i  11265  sqrtmsqi  11266  sqrtsqi  11267  sqsqrti  11268  sqrtge0i  11269  absidi  11270  absnidi  11271  xrmaxiflemlub  11391  serclim0  11448  fsum2d  11578  fsumcnv  11580  fsumconst  11597  modfsummodlem1  11599  fsumabs  11608  binom11  11629  prodf1  11685  prodfclim1  11687  prodsnf  11735  fprod2d  11766  fprodcnv  11768  efzval  11826  eftlub  11833  efsep  11834  ef4p  11837  efgt1  11840  reef11  11842  sinf  11847  cosf  11848  efi4p  11860  sinneg  11869  cosneg  11870  efival  11875  efmival  11876  cos01gt0  11906  sin02gt0  11907  absefib  11914  efieq1re  11915  demoivre  11916  demoivreALT  11917  eirraplem  11920  0dvds  11954  odd2np1lem  12013  odd2np1  12014  even2n  12015  mod2eq0even  12019  2teven  12028  opoe  12036  omoe  12037  opeo  12038  omeo  12039  m1exp1  12042  gcd0id  12116  gcdid0  12117  1gcd  12129  lcmdvds  12217  isprm2lem  12254  isprm3  12256  prmgt1  12270  coprm  12282  isevengcd2  12296  isoddgcd1  12297  sqpweven  12313  2sqpwodd  12314  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pythagtriplem16  12417  pc2dvds  12468  oddprmdvds  12492  pockthi  12496  1arith2  12506  unennn  12554  ctinfomlemom  12584  qnnen  12588  ssnnctlemct  12603  strslfv  12663  strle1g  12724  1strbas  12735  tgval  12873  ismgmn0  12941  mulgval  13192  mulgfng  13194  mulg0  13195  mulg1  13199  mulg2  13201  isnsg  13272  ringidvalg  13457  issrg  13461  subrgpropd  13749  rrgval  13758  islmod  13787  scaffvalg  13802  islssm  13853  sraval  13933  zrhval  14105  zrhvalg  14106  zrhex  14109  psrbag  14155  istopon  14181  eltg4i  14223  eltg3  14225  tg1  14227  tg2  14228  topnex  14254  cldrcl  14270  restsn  14348  lmrcl  14359  metflem  14517  xmetf  14518  ismet2  14522  xmeteq0  14527  xmettri2  14529  xmetpsmet  14537  xmetres2  14547  blfvalps  14553  blex  14555  blvalps  14556  blval  14557  blfps  14577  blf  14578  mopnval  14610  cnbl0  14702  cnblcld  14703  blssioo  14713  resubmet  14716  cncfmet  14747  cnplimcim  14821  cnlimcim  14825  cnlimc  14826  dvfgg  14842  dvfpm  14843  dvfcnpm  14844  dvcj  14858  reeff1olem  14906  ef2kpi  14941  sinperlem  14943  sin2kpi  14946  cos2kpi  14947  sinhalfpip  14955  sinhalfpim  14956  coshalfpip  14957  coshalfpim  14958  sincosq1sgn  14961  sinq12gt0  14965  sinkpi  14982  reeflog  14998  relogef  14999  logrpap0b  15011  loggt0b  15026  1cxp  15035  ecxp  15036  2logb9irrap  15109  lgsval2lem  15126  m1lgs  15192  djucllem  15292  bdrabexg  15398  bdunexb  15412  peano5set  15432  speano5  15436  bj-omtrans  15448  pwf1oexmid  15490  nninfsellemeq  15504  iswomninnlem  15539