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  7248  2dom  8961  limensuci  9075  frinsg  9653  djuen  10070  isfin1-3  10286  prlem934  10933  0idsr  10997  1idsr  10998  00sr  10999  addresr  11038  mulresr  11039  reclt1  12026  crne0  12127  nominpos  12367  fvf1tp  13697  expnass  14119  faclbnd2  14202  crim  15026  01sqrexlem1  15153  01sqrexlem7  15159  sqrt00  15174  sqreulem  15271  mulcn2  15507  ege2le3  16001  sin02gt0  16105  opoe  16278  oddprm  16726  pythagtriplem2  16733  pythagtriplem3  16734  pythagtriplem16  16746  pythagtrip  16750  pc1  16771  prmlem0  17021  acsfn0  17570  mgpress  20072  abvneg  20745  pmatcollpw3  22702  leordtval2  23130  txswaphmeo  23723  iccntr  24740  dvlipcn  25929  sinq34lt0t  26448  cosordlem  26469  efif1olem3  26483  lgamgulmlem2  26970  basellem3  27023  ppiub  27145  bposlem9  27233  lgsne0  27276  lgsdinn0  27286  chebbnd1  27413  eupth2lem3lem4  30215  mayete3i  31712  lnop0  31950  nmcexi  32010  nmoptrii  32078  nmopcoadji  32085  hstle1  32210  hst0  32217  strlem5  32239  jplem1  32252  vonf1owev  35175  subfacp1lem5  35251  limsucncmpi  36512  matunitlindflem1  37679  poimirlem15  37698  dvasin  37767  fdc  37808  eldioph3b  42885  oaabsb  43414  tfsconcatfv2  43460  omssaxinf2  45108  or2expropbi  47161  ich2exprop  47598  sprsymrelfolem2  47620  clnbgrisubgrgrim  48059  sinhpcosh  49868