Theorem mpanr12 705

Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Hypotheses

Ref	Expression
mpanr12.1	⊢ 𝜓
mpanr12.2	⊢ 𝜒
mpanr12.3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr12	⊢ (𝜑 → 𝜃)

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 ⊢ 𝜒
2		mpanr12.1	. . 3 ⊢ 𝜓
3		mpanr12.3	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	mpanr1 703	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 691	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:  wfisgOLD  6343  f1ofvswap  7298  2dom  9042  limensuci  9165  fiintOLD  9337  frinsg  9763  djuen  10182  isfin1-3  10398  prlem934  11045  0idsr  11109  1idsr  11110  00sr  11111  addresr  11150  mulresr  11151  reclt1  12135  crne0  12231  nominpos  12476  fvf1tp  13804  expnass  14224  faclbnd2  14307  crim  15132  01sqrexlem1  15259  01sqrexlem7  15265  sqrt00  15280  sqreulem  15376  mulcn2  15610  ege2le3  16104  sin02gt0  16208  opoe  16380  oddprm  16828  pythagtriplem2  16835  pythagtriplem3  16836  pythagtriplem16  16848  pythagtrip  16852  pc1  16873  prmlem0  17123  acsfn0  17670  mgpress  20108  abvneg  20784  pmatcollpw3  22720  leordtval2  23148  txswaphmeo  23741  iccntr  24759  dvlipcn  25949  sinq34lt0t  26468  cosordlem  26489  efif1olem3  26503  lgamgulmlem2  26990  basellem3  27043  ppiub  27165  bposlem9  27253  lgsne0  27296  lgsdinn0  27306  chebbnd1  27433  eupth2lem3lem4  30158  mayete3i  31655  lnop0  31893  nmcexi  31953  nmoptrii  32021  nmopcoadji  32028  hstle1  32153  hst0  32160  strlem5  32182  jplem1  32195  subfacp1lem5  35152  limsucncmpi  36409  matunitlindflem1  37586  poimirlem15  37605  dvasin  37674  fdc  37715  eldioph3b  42735  oaabsb  43265  tfsconcatfv2  43311  omssaxinf2  44961  or2expropbi  47011  ich2exprop  47433  sprsymrelfolem2  47455  clnbgrisubgrgrim  47893  sinhpcosh  49552