Theorem mp2an 696

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp2an.1	⊢ φ
mp2an.2	⊢ ψ
mp2an.3	⊢ ((φ ⋀ ψ) → χ)

Assertion

Ref	Expression
mp2an	⊢ χ

Proof of Theorem mp2an

Step	Hyp	Ref	Expression
1		mp2an.2	. 2 ⊢ ψ
2		mp2an.1	. . 3 ⊢ φ
3		mp2an.3	. . 3 ⊢ ((φ ⋀ ψ) → χ)
4	2, 3	mpan 694	. 2 ⊢ (ψ → χ)
5	1, 4	ax-mp 7	1 ⊢ χ

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  2false 718  mp3an 914  vtocl2 1839  cla42ev 1866  mosub 1918  sbccomg 1985  csbex 2005  sseq12i 2083  uneq12i 2178  ineq12i 2211  keephyp 2392  opeq12i 2488  breq12i 2623  opthwiener 2802  opelopab 2815  brab 2816  onssel 3104  onun 3105  onsucss 3106  tfis 3122  finds 3151  finds2 3153  onnev 3237  eqrelriv 3246  xpex 3255  opelcnv 3293  brcnv 3294  asymref 3431  intirr 3433  ssrnres 3473  cores 3491  coexg 3516  coex 3517  opabex 3601  fcoi1 3636  fcoi2 3637  fcnvres 3639  fabex 3645  fvopabf 3780  fopabcos 3824  fopabsn 3831  fvi 3833  fvresex 3848  abrexexlem2 3850  iunex 3854  tz7.44-2 3920  tz7.44-3 3921  tz7.48-2 3948  oprabss 3997  oprabex 4010  oprabex2 4012  1st2val 4085  2nd2val 4086  2ndconst 4087  df1st2 4116  df2nd2 4117  oawordeulem 4178  nneob 4245  ecoprcom 4309  ecoprass 4310  ecoprdi 4311  fnmap 4319  mapval 4322  elmap 4324  elpm 4326  entr 4403  endisj 4423  xpen 4474  pwen 4489  0sdom1dom 4510  unfilem1 4530  prfi 4537  fodomfi 4546  pwfi 4551  pm54.43 4552  en2lp 4582  inf0 4586  axinf2 4604  dfom3 4610  oancom 4613  infensuc 4618  trcl 4625  rankr1 4654  rankel 4660  rankss 4668  rankpr 4672  rankval4 4682  rankxplim 4692  rankxplim3 4694  scottex 4696  aceq3lem 4712  ac6lem 4734  numthlem 4763  zorn2lem1 4768  zorn2lem4 4771  cardon 4807  cardid 4808  carden 4811  carddom 4816  cardsdom 4817  domtri 4818  unxpdomlem 4823  unxpdom2 4825  sucxpdom 4826  cardprc 4841  alephsucpw 4850  aleph1 4851  alephord 4855  alephord3 4858  alephgeom 4862  alephfplem1 4876  alephfplem4 4879  alephfp2 4881  alephval2 4882  dominf 4884  cfom 4896  cdaval 4900  uncdadom 4901  pm110.643 4903  cdaen 4904  cda1en 4906  cdacomen 4909  cdaassen 4910  xpcdaen 4911  mapcdaen 4912  cdadom1 4913  cdadom3 4915  cdainf 4917  1lt2pi 5012  1q 5037  1lt2pq 5058  halfpq 5062  distrlem5pr 5111  0r 5169  1r 5170  m1r 5171  m1p1sr 5181  m1m1sr 5182  0lt1sr 5184  1ne0sr 5185  1idsr 5187  recexsrlem 5192  mappsrpr 5198  axresscn 5248  axi2m1 5265  addex 5297  mulex 5298  addcl 5300  mulcl 5301  addcom 5302  mulcom 5303  readdcl 5314  remulcl 5315  add4 5322  subcl 5346  subadd 5351  pncan3 5358  subneg 5384  subeq0 5385  mul4 5405  muladd 5406  resubcl 5419  addsub4 5454  xrltnrt 5522  mnfltpnf 5525  lttri2 5553  lttri3 5554  letri3 5555  leloe 5556  ltlen 5557  ltnsym 5558  lenlt 5559  ltle 5561  ltneOLD 5565  addgt0i 5583  mulgt0 5588  mulgt0i 5590  ltaddpos 5645  posdif 5646  ltnegcon1 5647  lenegcon1 5648  subge0 5657  recex 5666  muln0 5676  mulnzcnopr 5679  divval 5681  div0 5735  divmuldiv 5750  divadddiv 5752  divdivdiv 5753  redivcl 5762  recgt0i 5778  ltdiv23i 5851  nnssre 5883  nnind 5893  0nnn 5904  2nn 5954  3nn 5955  4nn 5957  8th4div3 5986  halfpm6th 5987  xrsupsslem 6031  xrinfmsslem 6032  xrsup0 6052  nn0addcl 6076  nn0mulcl 6077  nn0addge1 6087  nn0addge2 6088  halfnz 6149  dfuz 6158  uzindOLD 6164  om2uzran 6245  uzrdgini 6248  uzrdgfnuz 6251  seq1val 6257  seq1res 6272  ser1cl1 6275  ser1recl 6276  ser1ref 6277  ser1mono 6282  ser1add2 6283  ser1add 6284  shftidt 6300  seq1shftid 6301  ioomax 6333  ioopos 6334  icoshftf1oi 6350  icounlem 6353  snunioolem 6355  eluzaddi 6376  eluzsubi 6377  uzinfm 6402  fzshftralt 6462  seq0fval 6475  seqzfval 6477  seqzfn 6479  seq1seqz 6481  seq1seq0t 6484  seq1seq0 6485  seq0fn 6486  seq00 6490  serzcl1 6502  dfseq0 6503  ser0cl1 6504  ser0f 6505  sqmul 6555  sumsqne0 6573  cu2 6579  subsq 6585  nnsqcl 6598  nn0le2msqt 6601  nn0opthlem1 6602  nn0opth 6604  sqr0 6610  sqrlem1 6611  sqrlem2 6612  sqrlem6 6616  sqrlem8 6618  sqrlem13 6623  sqrlem24 6634  sqrgt0i 6635  sqrlem26 6636  sqrmuli 6642  sqr4 6655  sqr9 6656  sqr2gt1lt2 6657  sqr2irrlem1 6662  sqr2irrlem4 6665  i3 6671  nthruc 6684  nthruz 6685  crre 6714  crreOLD 6715  crim 6716  crimOLD 6717  cjmulge0 6736  abs00 6785  sqabsadd 6793  sqabssub 6794  abstri 6837  seq1bnd 6855  seq1ublem 6856  seq1ub 6857  ser1absdiflem 6874  fac1 6880  facp1t 6881  faclbnd4lem1 6893  bcpasc2 6913  bcpasc 6915  sumeq2 6931  fsump1s 6959  csbfsumlem 6972  fsumrev 6975  fsumshft 6977  serzref 6997  serzmulc 7004  ser0mulc 7005  ser1mulc 7006  binomlem6 7017  binom 7018  climunii 7043  climshft2 7051  climuz0 7053  climaddc 7076  climmulc 7077  iserzshft 7088  clim2serz 7089  climserzle 7091  climabslem 7092  climubi 7097  climsup 7099  climcau 7100  caucvglem2 7102  caucvg 7107  caucvg3a 7108  caucvg2 7109  caucvg3lem 7110  caucvg3t 7112  serzf0 7113  ser1f0 7114  ser1clim0 7117  ser1cmp 7118  ser1cmp0 7119  ser1cmp2 7121  iserzabslem 7122  cvgcmp2lem 7124  cvgcmp2clem 7126  cvgcmpub 7129  cvgcmp3c 7130  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  isumshft 7147  isumshft2 7148  isumsplit 7159  isum0split 7160  infcvgaux1 7162  infcvglem2 7165  fnsmnt 7169  expcnvlem1 7170  expcnvlem2 7171  expcnvlem4 7173  geoser 7177  geolimilem 7178  geolim1i 7181  georeclim 7183  0.999... 7189  cvgratlem1ALT 7190  cvgratlem2ALT 7191  fsum0diag 7201  fsum0diag2 7202  negfcncf 7212  abscncflem 7217  ivthlem1 7224  ivthlem4 7227  ivthlem5 7228  ivthlem6 7229  ivthlem7 7230  ivthlem8 7231  ivthlem9 7232  isupivth 7233  ivthlem4OLD 7236  ivthlem5OLD 7237  ivthlem6OLD 7238  ivthlem7OLD 7239  ivthlem8OLD 7240  ivthOLD 7241  ivth2OLD 7242  efcltlem1 7254  dfef2 7257  erelem6 7274  efcj 7286  efaddlem3 7290  efaddlem6 7293  efaddlem7 7294  efaddlem8 7295  efaddlem10 7297  efaddlem12 7299  efaddlem13 7300  efaddlem16 7303  efaddlem17 7304  efaddlem18 7305  efaddlem19 7306  efaddlem20 7307  efaddlem21 7308  efaddlem22 7309  efaddlem25 7312  efaddlem26 7313  efaddlem27 7314  ef1tllem 7331  ef01tllem1 7333  ef01tllem2 7334  ef01tlub 7335  absef01tllem 7336  absef01tlub 7337  eirrlem1 7338  eirrlem2 7339  eirrlem3 7340  eirrlem4 7341  eirrlem5 7342  abspef01tlub 7344  efsep 7345  efgt0 7353  eflt 7355  eflegeolem2 7362  efm1legeo 7365  efcnlem1 7367  efcn 7371  reeff1olem1 7372  reeff1olem1OLD 7374  sinadd 7401  cosadd 7402  sin01bndlem1 7417  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  cos1bnd 7424  cos2bnd 7425  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  sincos1sgn 7429  sincos2sgn 7430  acdc2lem2 7439  acdc5lem2 7442  xpnnen 7449  xpomen 7450  znnen 7453  qnnen 7454  infpn2 7460  ruclem5 7465  ruclem13 7473  ruclem15 7475  ruclem17 7477  ruclem22 7482  ruclem23 7483  ruclem24 7484  ruclem25 7485  ruclem26 7486  ruclem27 7487  ruclem28 7488  ruclem29 7489  ruclem30 7490  ruclem31 7491  ruclem32 7492  ruclem33 7493  ruclem35 7495  ruclem39 7499  resdomq 7501  aleph1re 7502  infxpidmlem9 7511  infxpidmlem12 7514  infcda 7518  infdif 7519  infdif2 7520  infxp 7523  infmap1 7524  iunctb 7525  aleph1irr 7528  qdensere 7701  ismeti 7752  cnmetba 7855  cnmet 7856  cncfmet 7857  cncfmet1 7858  remetba 7861  tgioo 7867  dscmet 7870  lmbrf 7882  iscauf 7891  iscau5 7893  lmsslem 7903  caussi 7905  lmclimnn 7915  xpcn 7926  fsumcnlem 7939  bcth 7982  isgrpi 7992  grprn 8006  isgrp2i 8026  issubgi 8074  ghgrpilem4 8088  ghsubgi 8090  cnring 8114  ringsn 8115  vsfval 8206  nvcli 8240  cnnvnm 8263  nmcnilem 8285  abscn 8290  abscncfALT 8291  va1cnlem 8292  sm1cnilem 8294  ipid 8310  ipcl 8312  lnocoi 8365  nmlno0lem 8398  nmlno0i 8399  nmblolbi 8404  isblo3i 8405  blocni 8409  blocn 8411  ip0i 8428  ip1ilem 8429  ip2i 8431  ipdirilem 8432  ipasslem1 8434  ipasslem2 8435  ipasslem6 8439  ipasslem7 8440  ipasslem8 8441  ipasslem10 8443  ip2dii 8448  pythi 8454  siilem1 8455  siii 8457  ipblnfi 8460  ajfuni 8464  ubthi 8488  minveclem1 8489  minveclem3 8491  minveclem9 8497  minveclem10 8498  minveclem14 8502  minveclem19 8507  minveclem21 8509  minveclem25 8513  minveclem28 8516  minveclem29 8517  minvecex 8522  minveclem35 8523  minvecdist 8529  minveclem39 8531  htthlem12 8574  spwval2 8595  sincolem 8603  sincnlem 8604  sinco 8605  cosco 8606  pilem1 8609  pilem2 8610  pilem3 8611  pigt2lt4 8613  sinhalfpilem 8617  sincosq1lem 8639  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  sincos4thpi 8646  sincos6thpi 8647  cosh111lem1 8648  cosh111t 8651  efghgrpilem 8653  efif 8655  efifolem1 8656  efifolem2 8657  efifolem3 8658  efifolem4 8659  efifolem5 8660  efifolem6 8661  efifolem7 8662  efif1lem1 8664  efif1lem2 8665  efif1lem3 8666  efif1lem4 8667  efif1lem5 8668  efif1lem6 8669  efif1lem7 8670  circgrpOLD 8677  circgrp 8679  eff1i 8683  effoi 8684  resslogrn 8692  relogf1o 8696  log1 8705  loge 8706  pilog 8707  h2hcau 8788  h2hlm 8789  hvmulex 8820  hvmulcl 8823  hvaddcl 8827  hvcom 8828  hvsubval 8829  hvsubcl 8830  hvadd4 8864  hicl 8887  his1 8905  normlem6 8920  normlem7 8921  norm-ii 8943  normpyth 8948  hhip 8983  hhph 8984  bcsALT 8985  hlim0 9044  hlimcaui 9045  shsspwh 9057  hhssnm 9070  hhssabl 9071  hhssnv 9073  hhshsslem1 9076  hhshsslem2 9077  hhsssh2 9079  hhssvs 9081  hhssph 9083  occon2 9101  projlem2 9126  projlem3 9127  projlem4 9128  projlem5 9129  projlem6 9130  projlem8 9132  projlem13 9137  projlem14 9138  projlem15 9139  projlem18 9142  projlem28 9152  pjthlem1 9157  omlsilem 9182  pjpj0 9193  pjpjth 9197  pjop 9200  pjpo 9201  shsel 9218  shscl 9219  chjval 9261  shscom 9270  shsva 9271  shsel1 9272  shsel2 9273  shslej 9276  shjcom 9278  shjcl 9282  shlub 9284  shsumval2 9298  chsscon3 9322  chdmm1 9338  shjshs 9353  chabs1 9379  chabs2 9380  ledi 9397  span0 9403  spanun 9405  sshhococ 9407  chsup0 9409  h1de2 9414  spansnpj 9441  pjoml4 9470  cmbr 9473  fh1 9504  fh2 9505  nonbool 9536  5oa 9546  pjadd 9560  pjmul 9562  pjsslem 9564  pjdifnorm 9568  pjnel 9608  mayete3 9613  dfiop2 9619  hoeq 9627  hocof 9632  hoaddcl 9634  hosubcl 9635  honegsub 9662  hosubeq0 9692  ho01 9694  eigpos 9702  nmopsetn0 9732  nmfnsetn0 9745  hhlno 9766  hhnmo 9767  hhblo 9768  hh0o 9769  nmopneg 9828  0cnfn 9843  0lnfn 9848  nmop0 9849  nmfn0 9850  nmlnop0ALT 9858  lnopco0 9867  lnopeq0lem1 9868  lnopunilem2 9874  lnophmlem2 9880  nmcopexlem2 9890  lnopcon 9901  lnfn0 9909  nmcfnexlem2 9919  lnfncon 9928  nlelsh 9931  cnlnadjlem8 9945  cnlnadjlem9 9946  adjbd1o 9956  bdophs 9967  bdopco 9969  adjco 9971  nmopcoadj 9972  unierr 9975  idleop 10002  hmopidmpj 10018  pjssdif2 10040  pjssdif1 10041  pjima 10042  pjinvar 10057  pjcmmul1 10067  pjcmmul2 10068  stcltr1 10139  mdsl1 10185  mdslmd1 10193  mdsldmd1 10195  mdslmd3 10196  mdexch 10199  shatomistic 10225  hatomistic 10226  chpssat 10227  cvat 10230  cvbr3 10231  cvexchlem 10232  cvexch 10233  chrelat3 10236  mdsymlem6 10272  mdsym 10275  sumdmdi 10278  cmmd 10279  cmdmd 10280  sumdmd 10283  dmdbr6at 10285  mdcompl 10290  dmdcompl 10291  mddmdin0 10292  abs2sqle 10306  abs2sqlt 10307  abs2dif 10310  abs2difabs 10311  elghom 10318  ghomgrpilem1 10319  ghomgrpilem2 10320  ghomsn 10322  symgval 10337  symggrpi 10340  symgidi 10341  cayleylem2 10344  cayleylem3 10345  mapdiscn 10434  homcard 10462  subsp 10465  iintlem2 10513  1alg 10534  eloi 10539  1ded 10551  0alg 10569  0ded 10570  0cat 10571  1cat 10572  mrdmcd 10602

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain