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  3077  ac6sfi  7168  dju0en  7534  1qec  7719  ltaddnq  7738  halfnqq  7741  1idsr  8099  pn0sr  8102  ltm1sr  8108  muleqadd  8959  halfcl  9481  rehalfcl  9482  half0  9483  2halves  9484  halfpos2  9485  halfnneg2  9487  halfaddsub  9489  nneoor  9698  zeo  9701  fztp  10434  modqfrac  10723  iexpcyc  11030  bcn2  11151  bcpasc  11153  imre  11561  reim  11562  crim  11568  addcj  11601  imval2  11604  sinf  12415  efi4p  12428  resin4p  12429  recos4p  12430  sinneg  12437  efival  12443  cosadd  12448  sinmul  12455  sinbnd  12463  cosbnd  12464  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  odd2np1lem  12583  odd2np1  12584  pythagtriplem12  12998  pockthi  13081  opprsubrngg  14457  opprdomnbg  14521  isridl  14778  zlmval  14901  zlmlemg  14902  zlmsca  14906  zlmvscag  14907  mopnex  15496  sub1cncf  15593  sub2cncf  15594  sincosq1lem  15816  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  abssinper  15837  coskpi  15839  rpcxpsqrt  15913  logsqrt  15914  2lgsoddprmlem2  16105