Theorem mpanr12 721

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  wfisg  5715  2dom  8029  limensuci  8136  phplem4  8142  unfi  8227  fiint  8237  cdaen  8995  isfin1-3  9208  prlem934  9855  0idsr  9918  1idsr  9919  00sr  9920  addresr  9959  mulresr  9960  reclt1  10918  crne0  11013  nominpos  11269  expnass  12970  faclbnd2  13078  crim  13855  sqrlem1  13983  sqrlem7  13989  sqrt00  14004  sqreulem  14099  mulcn2  14326  ege2le3  14820  sin02gt0  14922  opoe  15087  oddprm  15515  pythagtriplem2  15522  pythagtriplem3  15523  pythagtriplem16  15535  pythagtrip  15539  pc1  15560  prmlem0  15812  acsfn0  16321  mgpress  18500  abvneg  18834  pmatcollpw3  20589  leordtval2  21016  txswaphmeo  21608  iccntr  22624  dvlipcn  23757  sinq34lt0t  24261  cosordlem  24277  efif1olem3  24290  lgamgulmlem2  24756  basellem3  24809  ppiub  24929  bposlem9  25017  lgsne0  25060  lgsdinn0  25070  chebbnd1  25161  eupth2lem3lem4  27091  mayete3i  28587  lnop0  28825  nmcexi  28885  nmoptrii  28953  nmopcoadji  28960  hstle1  29085  hst0  29092  strlem5  29114  jplem1  29127  cnvoprab  29498  subfacp1lem5  31166  frinsg  31742  limsucncmpi  32444  matunitlindflem1  33405  poimirlem15  33424  dvasin  33496  fdc  33541  eldioph3b  37328  sprsymrelfolem2  41743  sinhpcosh  42481