Theorem mpanl12 702

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reuun1  4280  frminex  5603  tz6.26i  6306  wfii  6308  tfr2ALT  8332  tfr3ALT  8333  opthreg  9527  unsnen  10463  axcnre  11075  addgt0  11623  addgegt0  11624  addgtge0  11625  addge0  11626  addgt0i  11676  addge0i  11677  addgegt0i  11678  add20i  11680  mulge0i  11684  recextlem1  11767  recne0  11809  recdiv  11847  rec11i  11882  recgt1  12038  prodgt0i  12049  xadddi2  13212  iccshftri  13403  iccshftli  13405  iccdili  13407  icccntri  13409  mulexpz  14025  expaddz  14029  m1expeven  14032  iexpcyc  14130  cnpart  15163  resqrex  15173  sqreulem  15283  amgm2  15293  rlim  15418  ello12  15439  elo12  15450  bpolylem  15971  ege2le3  16013  dvdslelem  16236  divalglem1  16321  divalglem6  16325  divalglem9  16328  gcdaddmlem  16451  sqnprm  16629  prmlem1  17035  prmlem2  17047  m1expaddsub  19427  psgnuni  19428  gzrngunitlem  21387  lmres  23244  zdis  24761  iihalf1  24881  lmclimf  25260  vitali  25570  ismbf  25585  ismbfcn  25586  mbfconst  25590  cncombf  25615  cnmbf  25616  limcfval  25829  dvnfre  25912  quotlem  26264  ulmval  26345  ulmpm  26348  abelthlem2  26398  abelthlem3  26399  abelthlem5  26401  abelthlem7  26404  efcvx  26415  logtayl  26625  logccv  26628  cxpcn3  26714  emcllem2  26963  zetacvg  26981  basellem5  27051  bposlem7  27257  chebbnd1lem3  27438  dchrisumlem3  27458  iscgrgd  28585  axcontlem2  29038  nv1  30750  blocnilem  30879  ipasslem8  30912  siii  30928  ubthlem1  30945  norm1  31324  hhshsslem2  31343  hoscli  31837  hodcli  31838  cnlnadjlem7  32148  adjbdln  32158  pjnmopi  32223  strlem1  32325  rexdiv  33007  tpr2rico  34069  qqhre  34177  signsply0  34708  subfacval3  35383  erdszelem4  35388  erdszelem8  35392  elmrsubrn  35714  rdgprc  35986  fwddifval  36356  fwddifnval  36357  exrecfnlem  37580  poimirlem29  37846  ismblfin  37858  itg2addnclem  37868  caures  37957  sswfaxreg  45224  nthrucw  47126  cjnpoly  47131  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem4  48361  iooii  49159  icccldii  49160