Theorem mp3an23 1366

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	⊢ 𝜓
mp3an23.2	⊢ 𝜒
mp3an23.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 ⊢ 𝜓
2		mp3an23.2	. . 3 ⊢ 𝜒
3		mp3an23.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1363	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 425	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  sbciegf  3064  ac6sfi  7130  dju0en  7489  1qec  7668  ltaddnq  7687  halfnqq  7690  1idsr  8048  pn0sr  8051  ltm1sr  8057  muleqadd  8907  halfcl  9429  rehalfcl  9430  half0  9431  2halves  9432  halfpos2  9433  halfnneg2  9435  halfaddsub  9437  nneoor  9643  zeo  9646  fztp  10375  modqfrac  10662  iexpcyc  10969  bcn2  11089  bcpasc  11091  imre  11491  reim  11492  crim  11498  addcj  11531  imval2  11534  sinf  12345  efi4p  12358  resin4p  12359  recos4p  12360  sinneg  12367  efival  12373  cosadd  12378  sinmul  12385  sinbnd  12393  cosbnd  12394  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  sin01gt0  12403  cos01gt0  12404  sin02gt0  12405  odd2np1lem  12513  odd2np1  12514  pythagtriplem12  12928  pockthi  13011  opprsubrngg  14306  opprdomnbg  14370  isridl  14600  zlmval  14723  zlmlemg  14724  zlmsca  14728  zlmvscag  14729  mopnex  15316  sub1cncf  15413  sub2cncf  15414  sincosq1lem  15636  sincosq2sgn  15638  sincosq3sgn  15639  sincosq4sgn  15640  sinq12gt0  15641  abssinper  15657  coskpi  15659  rpcxpsqrt  15733  logsqrt  15734  2lgsoddprmlem2  15925