Theorem mpd3an3 1325

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2
mpd3an3.3

Assertion

Ref	Expression
mpd3an3

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2
2		mpd3an3.3	. . 3
3	2	3expa 1196	. 2
4	1, 3	mpdan 668	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  stoic2b  1608  elovmpt2  6520  f1oeng  7554  wdomimag  8034  cdaval  8571  gruuni  9199  genpv  9398  infmssuzle  11193  fzrevral3  11794  flflp1  11944  subsq2  12276  brfi1ind  12533  ccatws1ls  12637  swrdrlen  12659  swrd0swrdid  12689  2cshwid  12782  caubnd  13191  dvdsmul1  14005  dvdsmul2  14006  hashbcval  14520  setsvalg  14655  ressval  14684  restval  14824  mrelatglb0  15815  imasmnd2  15957  qusinv  16260  ghminv  16274  symgov  16415  gexod  16606  lsmvalx  16659  ringrz  17236  imasring  17268  irredneg  17359  evlrhm  18194  gsumsmonply1  18345  ocvin  18705  frlmiscvec  18884  mat1mhm  18986  marrepfval  19062  marrepval0  19063  marepvfval  19067  marepvval0  19068  1elcpmat  19216  m2cpminv0  19262  idpm2idmp  19302  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  restin  19667  qtopval  20196  elqtop3  20204  elfm3  20451  flimval  20464  nmge0  21136  nmeq0  21137  nminv  21140  nmo0  21242  0nghm  21248  coemulhi  22651  isosctrlem2  23153  divsqrtsumlem  23309  elghomlem1OLD  25363  rngorz  25404  nvge0  25577  nvnd  25594  dip0r  25630  dip0l  25631  nmoo0  25706  hi2eq  26022  resvval  27817  unitdivcld  27883  signspval  28509  ltflcei  30043  rngonegmn1l  30352  rngonegmn1r  30353  igenval  30458  pellfund14  30834  mendmulr  31137  fmuldfeq  31577  stoweidlem19  31801  stoweidlem26  31808  lincval1  33020  lfl0  34790  olj01  34950  olm11  34952  hl2at  35129  pmapeq0  35490  trlcl  35889  trlle  35909  tendoid  36499  tendo0plr  36518  tendoipl2  36524  erngmul  36532  erngmul-rN  36540  dvamulr  36738  dvavadd  36741  dvhmulr  36813  cdlemm10N  36845

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975