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 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  6386  f1ofvswap  7342  2dom  9095  limensuci  9219  phplem4OLD  9283  fiintOLD  9395  frinsg  9820  djuen  10239  isfin1-3  10455  prlem934  11102  0idsr  11166  1idsr  11167  00sr  11168  addresr  11207  mulresr  11208  reclt1  12190  crne0  12286  nominpos  12530  fvf1tp  13840  expnass  14257  faclbnd2  14340  crim  15164  01sqrexlem1  15291  01sqrexlem7  15297  sqrt00  15312  sqreulem  15408  mulcn2  15642  ege2le3  16138  sin02gt0  16240  opoe  16411  oddprm  16857  pythagtriplem2  16864  pythagtriplem3  16865  pythagtriplem16  16877  pythagtrip  16881  pc1  16902  prmlem0  17153  acsfn0  17718  mgpress  20176  mgpressOLD  20177  abvneg  20849  pmatcollpw3  22811  leordtval2  23241  txswaphmeo  23834  iccntr  24862  dvlipcn  26053  sinq34lt0t  26569  cosordlem  26590  efif1olem3  26604  lgamgulmlem2  27091  basellem3  27144  ppiub  27266  bposlem9  27354  lgsne0  27397  lgsdinn0  27407  chebbnd1  27534  eupth2lem3lem4  30263  mayete3i  31760  lnop0  31998  nmcexi  32058  nmoptrii  32126  nmopcoadji  32133  hstle1  32258  hst0  32265  strlem5  32287  jplem1  32300  cnvoprabOLD  32734  subfacp1lem5  35152  limsucncmpi  36411  matunitlindflem1  37576  poimirlem15  37595  dvasin  37664  fdc  37705  eldioph3b  42721  oaabsb  43256  tfsconcatfv2  43302  or2expropbi  46949  ich2exprop  47345  sprsymrelfolem2  47367  clnbgrisubgrgrim  47784  sinhpcosh  48832