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

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 ⊢ 𝜓
2		mpanl12.1	. . 3 ⊢ 𝜑
3		mpanl12.3	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpanl1 699	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 689	1 ⊢ (𝜒 → 𝜃)

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  4237  frminex  5499  tz6.26i  6148  wfii  6150  opthreg  9065  unsnen  9964  axcnre  10575  addgt0  11115  addgegt0  11116  addgtge0  11117  addge0  11118  addgt0i  11168  addge0i  11169  addgegt0i  11170  add20i  11172  mulge0i  11176  recextlem1  11259  recne0  11300  recdiv  11335  rec11i  11370  recgt1  11525  prodgt0i  11536  xadddi2  12678  iccshftri  12865  iccshftli  12867  iccdili  12869  icccntri  12871  mulexpz  13465  expaddz  13469  m1expeven  13472  iexpcyc  13565  cnpart  14591  resqrex  14602  sqreulem  14711  amgm2  14721  rlim  14844  ello12  14865  elo12  14876  ege2le3  15435  dvdslelem  15651  divalglem1  15735  divalglem6  15739  divalglem9  15742  gcdaddmlem  15862  sqnprm  16036  prmlem1  16433  prmlem2  16445  m1expaddsub  18618  psgnuni  18619  gzrngunitlem  20156  lmres  21905  zdis  23421  iihalf1  23536  lmclimf  23908  vitali  24217  ismbf  24232  ismbfcn  24233  mbfconst  24237  cncombf  24262  cnmbf  24263  limcfval  24475  dvnfre  24555  quotlem  24896  ulmval  24975  ulmpm  24978  abelthlem2  25027  abelthlem3  25028  abelthlem5  25030  abelthlem7  25033  efcvx  25044  logtayl  25251  logccv  25254  cxpcn3  25337  emcllem2  25582  zetacvg  25600  basellem5  25670  bposlem7  25874  chebbnd1lem3  26055  dchrisumlem3  26075  iscgrgd  26307  axcontlem2  26759  nv1  28458  blocnilem  28587  ipasslem8  28620  siii  28636  ubthlem1  28653  norm1  29032  hhshsslem2  29051  hoscli  29545  hodcli  29546  cnlnadjlem7  29856  adjbdln  29866  pjnmopi  29931  strlem1  30033  rexdiv  30628  tpr2rico  31265  qqhre  31371  signsply0  31931  subfacval3  32549  erdszelem4  32554  erdszelem8  32558  elmrsubrn  32880  rdgprc  33152  frindi  33199  fwddifval  33736  fwddifnval  33737  exrecfnlem  34796  poimirlem29  35086  ismblfin  35098  itg2addnclem  35108  caures  35198