MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpanr12 Structured version   Visualization version   GIF version

Theorem mpanr12 701
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1 𝜓
mpanr12.2 𝜒
mpanr12.3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr12 (𝜑𝜃)

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2 𝜒
2 mpanr12.1 . . 3 𝜓
3 mpanr12.3 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3mpanr1 699 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 687 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  wfisg  6182  2dom  8576  limensuci  8687  phplem4  8693  unfi  8779  fiint  8789  djuen  9589  isfin1-3  9802  prlem934  10449  0idsr  10513  1idsr  10514  00sr  10515  addresr  10554  mulresr  10555  reclt1  11529  crne0  11625  nominpos  11868  expnass  13565  faclbnd2  13646  crim  14469  sqrlem1  14597  sqrlem7  14603  sqrt00  14618  sqreulem  14714  mulcn2  14947  ege2le3  15438  sin02gt0  15540  opoe  15707  oddprm  16142  pythagtriplem2  16149  pythagtriplem3  16150  pythagtriplem16  16162  pythagtrip  16166  pc1  16187  prmlem0  16434  acsfn0  16926  mgpress  19186  abvneg  19541  pmatcollpw3  21327  leordtval2  21755  txswaphmeo  22348  iccntr  23363  dvlipcn  24525  sinq34lt0t  25029  cosordlem  25047  efif1olem3  25060  lgamgulmlem2  25540  basellem3  25593  ppiub  25713  bposlem9  25801  lgsne0  25844  lgsdinn0  25854  chebbnd1  25981  eupth2lem3lem4  27943  mayete3i  29438  lnop0  29676  nmcexi  29736  nmoptrii  29804  nmopcoadji  29811  hstle1  29936  hst0  29943  strlem5  29965  jplem1  29978  cnvoprabOLD  30388  subfacp1lem5  32334  frinsg  32990  limsucncmpi  33696  matunitlindflem1  34774  poimirlem15  34793  dvasin  34864  fdc  34907  eldioph3b  39246  or2expropbi  43154  ich2exprop  43484  sprsymrelfolem2  43506  sinhpcosh  44741
  Copyright terms: Public domain W3C validator