Theorem mpanl12 698

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  reuun1  4316  frminex  5655  tz6.26i  6349  wfii  6352  wfr3OLD  8340  tfr2ALT  8403  tfr3ALT  8404  opthreg  9615  unsnen  10550  axcnre  11161  addgt0  11704  addgegt0  11705  addgtge0  11706  addge0  11707  addgt0i  11757  addge0i  11758  addgegt0i  11759  add20i  11761  mulge0i  11765  recextlem1  11848  recne0  11889  recdiv  11924  rec11i  11959  recgt1  12114  prodgt0i  12125  xadddi2  13280  iccshftri  13468  iccshftli  13470  iccdili  13472  icccntri  13474  mulexpz  14072  expaddz  14076  m1expeven  14079  iexpcyc  14175  cnpart  15191  resqrex  15201  sqreulem  15310  amgm2  15320  rlim  15443  ello12  15464  elo12  15475  bpolylem  15996  ege2le3  16037  dvdslelem  16256  divalglem1  16341  divalglem6  16345  divalglem9  16348  gcdaddmlem  16469  sqnprm  16643  prmlem1  17045  prmlem2  17057  m1expaddsub  19407  psgnuni  19408  gzrngunitlem  21210  lmres  23024  zdis  24552  iihalf1  24672  lmclimf  25052  vitali  25362  ismbf  25377  ismbfcn  25378  mbfconst  25382  cncombf  25407  cnmbf  25408  limcfval  25621  dvnfre  25704  quotlem  26049  ulmval  26128  ulmpm  26131  abelthlem2  26180  abelthlem3  26181  abelthlem5  26183  abelthlem7  26186  efcvx  26197  logtayl  26404  logccv  26407  cxpcn3  26492  emcllem2  26737  zetacvg  26755  basellem5  26825  bposlem7  27029  chebbnd1lem3  27210  dchrisumlem3  27230  iscgrgd  28031  axcontlem2  28490  nv1  30195  blocnilem  30324  ipasslem8  30357  siii  30373  ubthlem1  30390  norm1  30769  hhshsslem2  30788  hoscli  31282  hodcli  31283  cnlnadjlem7  31593  adjbdln  31603  pjnmopi  31668  strlem1  31770  rexdiv  32359  tpr2rico  33190  qqhre  33298  signsply0  33860  subfacval3  34478  erdszelem4  34483  erdszelem8  34487  elmrsubrn  34809  rdgprc  35070  fwddifval  35438  fwddifnval  35439  exrecfnlem  36563  poimirlem29  36820  ismblfin  36832  itg2addnclem  36842  caures  36931  iooii  47637  icccldii  47638