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

Theorem mpanl12 717
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 715 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 705 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  reuun1  3901  frminex  5084  tz6.26i  5700  wfii  5702  opthreg  8500  unsnen  9360  axcnre  9970  addgt0  10499  addgegt0  10500  addgtge0  10501  addge0  10502  addgt0i  10552  addge0i  10553  addgegt0i  10554  add20i  10556  mulge0i  10560  recextlem1  10642  recne0  10683  recdiv  10716  rec11i  10751  recgt1  10904  prodgt0i  10915  prodge0i  10916  xadddi2  12112  iccshftri  12292  iccshftli  12294  iccdili  12296  icccntri  12298  mulexpz  12883  expaddz  12887  m1expeven  12890  iexpcyc  12952  cnpart  13961  resqrex  13972  sqreulem  14080  amgm2  14090  rlim  14207  ello12  14228  elo12  14239  efcllem  14789  ege2le3  14801  dvdslelem  15012  divalglem1  15098  divalglem6  15102  divalglem9  15105  gcdaddmlem  15226  sqnprm  15395  prmlem1  15795  prmlem2  15808  xpscfn  16200  m1expaddsub  17899  psgnuni  17900  gzrngunitlem  19792  lmres  21085  zdis  22600  iihalf1  22711  lmclimf  23083  vitali  23363  ismbf  23378  ismbfcn  23379  mbfconst  23383  cncombf  23406  cnmbf  23407  limcfval  23617  dvnfre  23696  quotlem  24036  ulmval  24115  ulmpm  24118  abelthlem2  24167  abelthlem3  24168  abelthlem5  24170  abelthlem7  24173  efcvx  24184  logtayl  24387  logccv  24390  cxpcn3  24470  emcllem2  24704  zetacvg  24722  basellem5  24792  bposlem7  24996  chebbnd1lem3  25141  dchrisumlem3  25161  iscgrgd  25389  axcontlem2  25826  nv1  27500  blocnilem  27629  ipasslem8  27662  siii  27678  ubthlem1  27696  norm1  28076  hhshsslem2  28095  hoscli  28591  hodcli  28592  cnlnadjlem7  28902  adjbdln  28912  pjnmopi  28977  strlem1  29079  rexdiv  29608  tpr2rico  29932  qqhre  30038  signsply0  30602  subfacval3  31145  erdszelem4  31150  erdszelem8  31154  elmrsubrn  31391  rdgprc  31674  frindi  31715  fwddifval  32244  fwddifnval  32245  poimirlem29  33409  ismblfin  33421  itg2addnclem  33432  caures  33527
  Copyright terms: Public domain W3C validator