Theorem mpanr12 704

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 702	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 690	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  wfisg  6151  2dom  8565  limensuci  8677  phplem4  8683  unfi  8769  fiint  8779  djuen  9580  isfin1-3  9797  prlem934  10444  0idsr  10508  1idsr  10509  00sr  10510  addresr  10549  mulresr  10550  reclt1  11524  crne0  11618  nominpos  11862  expnass  13566  faclbnd2  13647  crim  14466  sqrlem1  14594  sqrlem7  14600  sqrt00  14615  sqreulem  14711  mulcn2  14944  ege2le3  15435  sin02gt0  15537  opoe  15704  oddprm  16137  pythagtriplem2  16144  pythagtriplem3  16145  pythagtriplem16  16157  pythagtrip  16161  pc1  16182  prmlem0  16431  acsfn0  16923  mgpress  19243  abvneg  19598  pmatcollpw3  21389  leordtval2  21817  txswaphmeo  22410  iccntr  23426  dvlipcn  24597  sinq34lt0t  25102  cosordlem  25122  efif1olem3  25136  lgamgulmlem2  25615  basellem3  25668  ppiub  25788  bposlem9  25876  lgsne0  25919  lgsdinn0  25929  chebbnd1  26056  eupth2lem3lem4  28016  mayete3i  29511  lnop0  29749  nmcexi  29809  nmoptrii  29877  nmopcoadji  29884  hstle1  30009  hst0  30016  strlem5  30038  jplem1  30051  cnvoprabOLD  30482  subfacp1lem5  32544  frinsg  33200  limsucncmpi  33906  matunitlindflem1  35053  poimirlem15  35072  dvasin  35141  fdc  35183  eldioph3b  39706  or2expropbi  43626  ich2exprop  43988  sprsymrelfolem2  44010  sinhpcosh  45266