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

Theorem mpanl12 713
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mpanl12.1 𝜑
mpanl12.2 𝜓
mpanl12.3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
mpanl12 (𝜒𝜃)

Proof of Theorem mpanl12
StepHypRef Expression
1 mpanl12.2 . 2 𝜓
2 mpanl12.1 . . 3 𝜑
3 mpanl12.3 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3mpanl1 711 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 701 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  reuun1  3864  frminex  5005  tz6.26i  5612  wfii  5614  opthreg  8372  unsnen  9228  axcnre  9838  addgt0  10360  addgegt0  10361  addgtge0  10362  addge0  10363  addgt0i  10413  addge0i  10414  addgegt0i  10415  add20i  10417  mulge0i  10421  recextlem1  10503  recne0  10544  recdiv  10577  rec11i  10612  recgt1  10765  prodgt0i  10776  prodge0i  10777  xadddi2  11953  iccshftri  12131  iccshftli  12133  iccdili  12135  icccntri  12137  mulexpz  12714  expaddz  12718  m1expeven  12721  iexpcyc  12783  cnpart  13771  resqrex  13782  sqreulem  13890  amgm2  13900  rlim  14017  ello12  14038  elo12  14049  efcllem  14590  ege2le3  14602  dvdslelem  14812  divalglem1  14898  divalglem6  14902  divalglem9  14905  gcdaddmlem  15026  sqnprm  15195  prmlem1  15595  prmlem2  15608  xpscfn  15985  m1expaddsub  17684  psgnuni  17685  gzrngunitlem  19573  lmres  20853  zdis  22356  iihalf1  22466  lmclimf  22824  vitali  23102  ismbf  23117  ismbfcn  23118  mbfconst  23122  cncombf  23145  cnmbf  23146  limcfval  23356  dvnfre  23435  quotlem  23773  ulmval  23852  ulmpm  23855  abelthlem2  23904  abelthlem3  23905  abelthlem5  23907  abelthlem7  23910  efcvx  23921  logtayl  24120  logccv  24123  cxpcn3  24203  emcllem2  24437  zetacvg  24455  basellem5  24525  bposlem7  24729  chebbnd1lem3  24874  dchrisumlem3  24894  iscgrgd  25123  axcontlem2  25560  nv1  26706  blocnilem  26846  ipasslem8  26879  siii  26895  ubthlem1  26913  norm1  27293  hhshsslem2  27312  hoscli  27808  hodcli  27809  cnlnadjlem7  28119  adjbdln  28129  pjnmopi  28194  strlem1  28296  rexdiv  28768  tpr2rico  29089  qqhre  29195  signsply0  29757  subfacval3  30228  erdszelem4  30233  erdszelem8  30237  elmrsubrn  30474  rdgprc  30747  frindi  30788  fwddifval  31242  fwddifnval  31243  poimirlem29  32408  ismblfin  32420  itg2addnclem  32431  caures  32526
  Copyright terms: Public domain W3C validator