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

Theorem mpanl12 701
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 699 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 689 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  reuun1  4270  frminex  5522  tz6.26i  6167  wfii  6169  opthreg  9078  unsnen  9973  axcnre  10584  addgt0  11124  addgegt0  11125  addgtge0  11126  addge0  11127  addgt0i  11177  addge0i  11178  addgegt0i  11179  add20i  11181  mulge0i  11185  recextlem1  11268  recne0  11309  recdiv  11344  rec11i  11379  recgt1  11534  prodgt0i  11545  xadddi2  12687  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  mulexpz  13474  expaddz  13478  m1expeven  13481  iexpcyc  13574  cnpart  14599  resqrex  14610  sqreulem  14719  amgm2  14729  rlim  14852  ello12  14873  elo12  14884  ege2le3  15443  dvdslelem  15659  divalglem1  15743  divalglem6  15747  divalglem9  15750  gcdaddmlem  15870  sqnprm  16044  prmlem1  16441  prmlem2  16453  m1expaddsub  18626  psgnuni  18627  gzrngunitlem  20610  lmres  21908  zdis  23424  iihalf1  23539  lmclimf  23911  vitali  24220  ismbf  24235  ismbfcn  24236  mbfconst  24240  cncombf  24265  cnmbf  24266  limcfval  24478  dvnfre  24558  quotlem  24899  ulmval  24978  ulmpm  24981  abelthlem2  25030  abelthlem3  25031  abelthlem5  25033  abelthlem7  25036  efcvx  25047  logtayl  25254  logccv  25257  cxpcn3  25340  emcllem2  25585  zetacvg  25603  basellem5  25673  bposlem7  25877  chebbnd1lem3  26058  dchrisumlem3  26078  iscgrgd  26310  axcontlem2  26762  nv1  28461  blocnilem  28590  ipasslem8  28623  siii  28639  ubthlem1  28656  norm1  29035  hhshsslem2  29054  hoscli  29548  hodcli  29549  cnlnadjlem7  29859  adjbdln  29869  pjnmopi  29934  strlem1  30036  rexdiv  30613  tpr2rico  31212  qqhre  31318  signsply0  31878  subfacval3  32493  erdszelem4  32498  erdszelem8  32502  elmrsubrn  32824  rdgprc  33096  frindi  33143  fwddifval  33680  fwddifnval  33681  exrecfnlem  34741  poimirlem29  35031  ismblfin  35043  itg2addnclem  35053  caures  35143
  Copyright terms: Public domain W3C validator