Theorem mpanl12 700

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 698	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 688	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  reuun1  4285  frminex  5535  tz6.26i  6180  wfii  6182  opthreg  9081  unsnen  9975  axcnre  10586  addgt0  11126  addgegt0  11127  addgtge0  11128  addge0  11129  addgt0i  11179  addge0i  11180  addgegt0i  11181  add20i  11183  mulge0i  11187  recextlem1  11270  recne0  11311  recdiv  11346  rec11i  11381  recgt1  11536  prodgt0i  11547  xadddi2  12691  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  mulexpz  13470  expaddz  13474  m1expeven  13477  iexpcyc  13570  cnpart  14599  resqrex  14610  sqreulem  14719  amgm2  14729  rlim  14852  ello12  14873  elo12  14884  ege2le3  15443  dvdslelem  15659  divalglem1  15745  divalglem6  15749  divalglem9  15752  gcdaddmlem  15872  sqnprm  16046  prmlem1  16441  prmlem2  16453  m1expaddsub  18626  psgnuni  18627  gzrngunitlem  20610  lmres  21908  zdis  23424  iihalf1  23535  lmclimf  23907  vitali  24214  ismbf  24229  ismbfcn  24230  mbfconst  24234  cncombf  24259  cnmbf  24260  limcfval  24470  dvnfre  24549  quotlem  24889  ulmval  24968  ulmpm  24971  abelthlem2  25020  abelthlem3  25021  abelthlem5  25023  abelthlem7  25026  efcvx  25037  logtayl  25243  logccv  25246  cxpcn3  25329  emcllem2  25574  zetacvg  25592  basellem5  25662  bposlem7  25866  chebbnd1lem3  26047  dchrisumlem3  26067  iscgrgd  26299  axcontlem2  26751  nv1  28452  blocnilem  28581  ipasslem8  28614  siii  28630  ubthlem1  28647  norm1  29026  hhshsslem2  29045  hoscli  29539  hodcli  29540  cnlnadjlem7  29850  adjbdln  29860  pjnmopi  29925  strlem1  30027  rexdiv  30602  tpr2rico  31155  qqhre  31261  signsply0  31821  subfacval3  32436  erdszelem4  32441  erdszelem8  32445  elmrsubrn  32767  rdgprc  33039  frindi  33086  fwddifval  33623  fwddifnval  33624  exrecfnlem  34663  poimirlem29  34936  ismblfin  34948  itg2addnclem  34958  caures  35050