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:  f1ofvswap  7247  2dom  8962  limensuci  9077  fiintOLD  9236  frinsg  9666  djuen  10083  isfin1-3  10299  prlem934  10946  0idsr  11010  1idsr  11011  00sr  11012  addresr  11051  mulresr  11052  reclt1  12038  crne0  12139  nominpos  12379  fvf1tp  13711  expnass  14133  faclbnd2  14216  crim  15040  01sqrexlem1  15167  01sqrexlem7  15173  sqrt00  15188  sqreulem  15285  mulcn2  15521  ege2le3  16015  sin02gt0  16119  opoe  16292  oddprm  16740  pythagtriplem2  16747  pythagtriplem3  16748  pythagtriplem16  16760  pythagtrip  16764  pc1  16785  prmlem0  17035  acsfn0  17584  mgpress  20053  abvneg  20729  pmatcollpw3  22687  leordtval2  23115  txswaphmeo  23708  iccntr  24726  dvlipcn  25915  sinq34lt0t  26434  cosordlem  26455  efif1olem3  26469  lgamgulmlem2  26956  basellem3  27009  ppiub  27131  bposlem9  27219  lgsne0  27262  lgsdinn0  27272  chebbnd1  27399  eupth2lem3lem4  30193  mayete3i  31690  lnop0  31928  nmcexi  31988  nmoptrii  32056  nmopcoadji  32063  hstle1  32188  hst0  32195  strlem5  32217  jplem1  32230  vonf1owev  35083  subfacp1lem5  35159  limsucncmpi  36421  matunitlindflem1  37598  poimirlem15  37617  dvasin  37686  fdc  37727  eldioph3b  42741  oaabsb  43270  tfsconcatfv2  43316  omssaxinf2  44965  or2expropbi  47022  ich2exprop  47459  sprsymrelfolem2  47481  clnbgrisubgrgrim  47920  sinhpcosh  49729