Theorem mpanr12 716

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

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  wfisg  5618  2dom  7892  limensuci  7998  phplem4  8004  unfi  8089  fiint  8099  cdaen  8855  isfin1-3  9068  prlem934  9711  0idsr  9774  1idsr  9775  00sr  9776  addresr  9815  mulresr  9816  reclt1  10767  crne0  10860  nominpos  11116  expnass  12787  faclbnd2  12895  crim  13649  sqrlem1  13777  sqrlem7  13783  sqrt00  13798  sqreulem  13893  mulcn2  14120  ege2le3  14605  sin02gt0  14707  opoe  14871  oddprm  15299  pythagtriplem2  15306  pythagtriplem3  15307  pythagtriplem16  15319  pythagtrip  15323  pc1  15344  prmlem0  15596  acsfn0  16090  mgpress  18269  abvneg  18603  pmatcollpw3  20350  leordtval2  20768  txswaphmeo  21360  iccntr  22364  dvlipcn  23478  sinq34lt0t  23982  cosordlem  23998  efif1olem3  24011  lgamgulmlem2  24473  basellem3  24526  ppiub  24646  bposlem9  24734  lgsne0  24777  lgsdinn0  24787  chebbnd1  24878  constr1trl  25884  constr2trl  25895  usgrcyclnl2  25935  4cycl4dv  25961  2spontn0vne  26180  eupath2lem3  26272  mayete3i  27777  lnop0  28015  nmcexi  28075  nmoptrii  28143  nmopcoadji  28150  hstle1  28275  hst0  28282  strlem5  28304  jplem1  28317  cnvoprab  28692  subfacp1lem5  30226  frinsg  30792  limsucncmpi  31420  matunitlindflem1  32378  poimirlem15  32397  dvasin  32469  fdc  32514  eldioph3b  36149  eupth2lem3lem4  41401  sinhpcosh  42243