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  4328  frminex  5664  tz6.26i  6370  wfii  6373  wfr3OLD  8378  tfr2ALT  8441  tfr3ALT  8442  opthreg  9658  unsnen  10593  axcnre  11204  addgt0  11749  addgegt0  11750  addgtge0  11751  addge0  11752  addgt0i  11802  addge0i  11803  addgegt0i  11804  add20i  11806  mulge0i  11810  recextlem1  11893  recne0  11935  recdiv  11973  rec11i  12008  recgt1  12164  prodgt0i  12175  xadddi2  13339  iccshftri  13527  iccshftli  13529  iccdili  13531  icccntri  13533  mulexpz  14143  expaddz  14147  m1expeven  14150  iexpcyc  14246  cnpart  15279  resqrex  15289  sqreulem  15398  amgm2  15408  rlim  15531  ello12  15552  elo12  15563  bpolylem  16084  ege2le3  16126  dvdslelem  16346  divalglem1  16431  divalglem6  16435  divalglem9  16438  gcdaddmlem  16561  sqnprm  16739  prmlem1  17145  prmlem2  17157  m1expaddsub  19516  psgnuni  19517  gzrngunitlem  21450  lmres  23308  zdis  24838  iihalf1  24958  lmclimf  25338  vitali  25648  ismbf  25663  ismbfcn  25664  mbfconst  25668  cncombf  25693  cnmbf  25694  limcfval  25907  dvnfre  25990  quotlem  26342  ulmval  26423  ulmpm  26426  abelthlem2  26476  abelthlem3  26477  abelthlem5  26479  abelthlem7  26482  efcvx  26493  logtayl  26702  logccv  26705  cxpcn3  26791  emcllem2  27040  zetacvg  27058  basellem5  27128  bposlem7  27334  chebbnd1lem3  27515  dchrisumlem3  27535  iscgrgd  28521  axcontlem2  28980  nv1  30694  blocnilem  30823  ipasslem8  30856  siii  30872  ubthlem1  30889  norm1  31268  hhshsslem2  31287  hoscli  31781  hodcli  31782  cnlnadjlem7  32092  adjbdln  32102  pjnmopi  32167  strlem1  32269  rexdiv  32908  tpr2rico  33911  qqhre  34021  signsply0  34566  subfacval3  35194  erdszelem4  35199  erdszelem8  35203  elmrsubrn  35525  rdgprc  35795  fwddifval  36163  fwddifnval  36164  exrecfnlem  37380  poimirlem29  37656  ismblfin  37668  itg2addnclem  37678  caures  37767  sswfaxreg  45004  iooii  48815  icccldii  48816