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  3074  ac6sfi  7155  dju0en  7521  1qec  7703  ltaddnq  7722  halfnqq  7725  1idsr  8083  pn0sr  8086  ltm1sr  8092  muleqadd  8942  halfcl  9464  rehalfcl  9465  half0  9466  2halves  9467  halfpos2  9468  halfnneg2  9470  halfaddsub  9472  nneoor  9680  zeo  9683  fztp  10412  modqfrac  10699  iexpcyc  11006  bcn2  11126  bcpasc  11128  imre  11536  reim  11537  crim  11543  addcj  11576  imval2  11579  sinf  12390  efi4p  12403  resin4p  12404  recos4p  12405  sinneg  12412  efival  12418  cosadd  12423  sinmul  12430  sinbnd  12438  cosbnd  12439  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  odd2np1lem  12558  odd2np1  12559  pythagtriplem12  12973  pockthi  13056  opprsubrngg  14356  opprdomnbg  14420  isridl  14652  zlmval  14775  zlmlemg  14776  zlmsca  14780  zlmvscag  14781  mopnex  15370  sub1cncf  15467  sub2cncf  15468  sincosq1lem  15690  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  abssinper  15711  coskpi  15713  rpcxpsqrt  15787  logsqrt  15788  2lgsoddprmlem2  15979