ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan GIF version

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
StepHypRef Expression
1 mpan.1 . . 3 𝜑
21a1i 9 . 2 (𝜓𝜑)
3 mpan.2 . 2 ((𝜑𝜓) → 𝜒)
42, 3mpancom 422 1 (𝜓𝜒)
Colors of variables: wff set class
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  1324  mp3an12  1327  mp3an13  1328  ax9o  1698  sbnfc2  3117  ssdifss  3265  undifss  3503  uneqdifeqim  3508  elssuni  3835  csbexa  4129  difexg  4141  rabexg  4143  abssexg  4179  snexg  4181  copsexg  4240  sotritric  4320  sotritrieq  4321  trsuc  4418  oneli  4424  unexb  4438  opeluu  4446  rabxfr  4466  reuhyp  4468  ordunisuc2r  4509  reg3exmid  4575  brrelex12i  4664  brrelex1i  4665  brrelex2i  4666  xpss2  4733  opabid2  4753  eliunxp  4761  releldmi  4861  relelrni  4862  dmexg  4886  rnexg  4887  elres  4938  resexg  4942  relbrcnvg  5002  brcodir  5011  sotri  5019  sotri2  5021  sotri3  5022  dfrel2  5074  coi1  5139  fco  5376  fssres  5386  fabexg  5398  fvopab3g  5584  mptrcl  5593  mpteqb  5601  elfvmptrab1  5605  ffvelcdmi  5645  fsn2  5685  dfmptg  5690  fvpr1  5715  fvconst2  5727  mptexg  5736  oprabid  5900  ovprc  5903  caovcl  6022  caovass  6028  caovdi  6047  elmpocl  6062  ofexg  6080  resfunexgALT  6102  fo1stresm  6155  fo2ndresm  6156  1stexg  6161  2ndexg  6162  elopabi  6189  mpoexxg  6204  mpoxopn0yelv  6233  rntpos  6251  smores  6286  tfr0dm  6316  tfrlemibxssdm  6321  tfrexlem  6328  tfr1onlembxssdm  6337  tfrcllembxssdm  6350  rdgruledefgg  6369  rdgruledefg  6370  rdgivallem  6375  rdgexg  6383  frec0g  6391  ordgt0ge1  6429  omfnex  6443  oeiv  6450  nna0r  6472  nnm0r  6473  nnsucsssuc  6486  nn2m  6521  nnaordex  6522  nnawordex  6523  ecdmn0m  6570  ecelqsi  6582  ecidg  6592  ectocl  6595  encv  6739  f1oen  6752  ssdomg  6771  map1  6805  fiprc  6808  xpdom1  6828  fict  6861  isinfinf  6890  ac6sfi  6891  xpfi  6922  en1eqsn  6940  fidcenumlemr  6947  fiss  6969  eqinfti  7012  djueq2  7033  djulclr  7041  djurclr  7042  djulcl  7043  djurcl  7044  djuf1olem  7045  djulclb  7047  inl11  7057  eldju1st  7063  1stinl  7066  2ndinl  7067  1stinr  7068  2ndinr  7069  ctssdccl  7103  isomnimap  7128  ismkvmap  7145  iswomnimap  7157  djucomen  7208  0nnq  7341  mulidnq  7366  archnqq  7394  prarloclemarch2  7396  nqnq0pi  7415  nq0m0r  7433  nq02m  7442  prarloclemlt  7470  prarloclemn  7476  prarloclem5  7477  addnqprllem  7504  addnqprulem  7505  appdivnq  7540  1idprl  7567  1idpru  7568  addextpr  7598  cauappcvgprlemdisj  7628  cauappcvgprlemloc  7629  cauappcvgprlemladdru  7633  cauappcvgprlemladdrl  7634  caucvgprlemnbj  7644  caucvgprlemloc  7652  caucvgprprlemnbj  7670  caucvgprprlemloc  7680  caucvgprprlemaddq  7685  suplocexprlemmu  7695  suplocexprlemru  7696  suplocexprlemloc  7698  suplocexprlemlub  7701  0nsr  7726  ltsosr  7741  recexgt0sr  7750  prsrpos  7762  caucvgsr  7779  mappsrprg  7781  suplocsrlem  7785  mulresr  7815  axcnre  7858  axpre-ltwlin  7860  mulid2  7933  0re  7935  axmulgt0  8006  ltnsym2  8025  eqlei  8028  ltnei  8038  muladd11  8067  cnegex  8112  0cnALT  8124  negcl  8134  negneg  8184  mul02  8321  mulm1  8334  lt0neg2  8403  le0neg2  8405  recexre  8512  recexgt0  8514  mulge0  8553  gt0ap0i  8561  recextlem1  8584  recexap  8586  recclapzi  8670  recap0apzi  8671  recidapzi  8672  divassapzi  8695  divmulapzi  8696  divdirapzi  8697  rerecclapzi  8709  ltp1  8777  recgt0i  8839  ltmul1i  8853  ltdiv1i  8854  ltmuldivi  8855  ltmul2i  8856  lemul1i  8857  lemul2i  8858  sup3exmid  8890  nngt1ne1  8930  nnrecre  8932  nn0ge0  9177  nn0addcl  9187  nn0mulcl  9188  zgt0ge1  9287  dfuzi  9339  eluzel2  9509  eluz2b1  9577  uz2m1nn  9581  elnn0dc  9587  elnndc  9588  nn01to3  9593  zq  9602  nnrecq  9621  rpge0  9640  rpreccl  9654  mnflt  9757  pnfnlt  9761  mnfle  9766  xrlelttr  9780  xrltletr  9781  xrletr  9782  xgepnf  9790  xlt0neg2  9813  xle0neg2  9815  xaddpnf2  9821  xaddmnf2  9823  xaddid2  9837  elioomnf  9942  ige3m2fz  10022  fzshftral  10081  ige2m1fz1  10082  1fv  10112  4fvwrd4  10113  rebtwn2zlemstep  10226  qbtwnxr  10231  btwnzge0  10273  zmodid2  10325  q2txmodxeq0  10357  frec2uzrand  10378  frecuzrdgtcl  10385  frecfzennn  10399  nn0ennn  10406  uzennn  10409  0exp  10528  sqgt0api  10578  subsq2  10600  qsqeqor  10603  bernneq  10613  faclbnd  10692  faclbnd2  10693  faclbnd3  10694  hashinfuni  10728  hashxp  10777  2shfti  10811  reim  10832  imcl  10834  crim  10838  caucvgre  10961  rennim  10982  resqrexlemdecn  10992  qabsor  11055  absimle  11064  sqrtthi  11099  sqrtcli  11100  sqrtgt0i  11101  sqrtmsqi  11102  sqrtsqi  11103  sqsqrti  11104  sqrtge0i  11105  absidi  11106  absnidi  11107  xrmaxiflemlub  11227  serclim0  11284  fsum2d  11414  fsumcnv  11416  fsumconst  11433  modfsummodlem1  11435  fsumabs  11444  binom11  11465  prodf1  11521  prodfclim1  11523  prodsnf  11571  fprod2d  11602  fprodcnv  11604  efzval  11662  eftlub  11669  efsep  11670  ef4p  11673  efgt1  11676  reef11  11678  sinf  11683  cosf  11684  efi4p  11696  sinneg  11705  cosneg  11706  efival  11711  efmival  11712  cos01gt0  11741  sin02gt0  11742  absefib  11749  efieq1re  11750  demoivre  11751  demoivreALT  11752  eirraplem  11755  0dvds  11789  odd2np1lem  11847  odd2np1  11848  even2n  11849  mod2eq0even  11853  2teven  11862  opoe  11870  omoe  11871  opeo  11872  omeo  11873  m1exp1  11876  gcd0id  11950  gcdid0  11951  1gcd  11963  lcmdvds  12049  isprm2lem  12086  isprm3  12088  prmgt1  12102  coprm  12114  isevengcd2  12128  isoddgcd1  12129  sqpweven  12145  2sqpwodd  12146  pythagtriplem12  12245  pythagtriplem13  12246  pythagtriplem14  12247  pythagtriplem16  12249  pc2dvds  12299  oddprmdvds  12322  pockthi  12326  1arith2  12336  unennn  12368  ctinfomlemom  12398  qnnen  12402  ssnnctlemct  12417  strslfv  12476  strle1g  12533  1strbas  12542  ismgmn0  12656  mulgval  12862  mulgfng  12863  mulg0  12864  mulg1  12866  mulg2  12868  ringidvalg  12957  issrg  12961  istopon  13144  tgval  13182  eltg4i  13188  eltg3  13190  tg1  13192  tg2  13193  topnex  13219  cldrcl  13235  restsn  13313  lmrcl  13324  metflem  13482  xmetf  13483  ismet2  13487  xmeteq0  13492  xmettri2  13494  xmetpsmet  13502  xmetres2  13512  blfvalps  13518  blex  13520  blvalps  13521  blval  13522  blfps  13542  blf  13543  mopnval  13575  cnbl0  13667  cnblcld  13668  blssioo  13678  resubmet  13681  cncfmet  13712  cnplimcim  13769  cnlimcim  13773  cnlimc  13774  dvfgg  13790  dvfpm  13791  dvfcnpm  13792  dvcj  13806  reeff1olem  13825  ef2kpi  13860  sinperlem  13862  sin2kpi  13865  cos2kpi  13866  sinhalfpip  13874  sinhalfpim  13875  coshalfpip  13876  coshalfpim  13877  sincosq1sgn  13880  sinq12gt0  13884  sinkpi  13901  reeflog  13917  relogef  13918  logrpap0b  13930  loggt0b  13945  1cxp  13954  ecxp  13955  2logb9irrap  14028  lgsval2lem  14044  djucllem  14174  bdrabexg  14280  bdunexb  14294  peano5set  14314  speano5  14318  bj-omtrans  14330  pwf1oexmid  14371  nninfsellemeq  14386  iswomninnlem  14420
  Copyright terms: Public domain W3C validator