Theorem mp3an12 1364

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

Hypotheses

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

Assertion

Ref	Expression
mp3an12	⊢ (𝜒 → 𝜃)

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 ⊢ 𝜓
2		mp3an12.1	. . 3 ⊢ 𝜑
3		mp3an12.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an1 1361	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 424	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:  mp3an12i  1378  ceqsralv  2845  brelrn  4990  funpr  5408  fpm  6915  ener  7019  0fsupp  7251  ltaddnq  7722  ltadd1sr  8091  map2psrprg  8120  mul02  8660  ltapi  8910  div0ap  8976  divclapzi  9021  divcanap1zi  9022  divcanap2zi  9023  divrecapzi  9024  divcanap3zi  9025  divcanap4zi  9026  divassapzi  9036  divmulapzi  9037  divdirapzi  9038  redivclapzi  9052  ltm1  9120  mulgt1  9137  recgt1i  9172  recreclt  9174  ltmul1i  9194  ltdiv1i  9195  ltmuldivi  9196  ltmul2i  9197  lemul1i  9198  lemul2i  9199  cju  9235  nnge1  9260  nngt0  9262  nnrecgt0  9275  elnnnn0c  9541  elnnz1  9600  recnz  9671  eluzsubi  9882  ge0gtmnf  10156  m1expcl2  10923  1exp  10930  m1expeven  10948  expubnd  10958  iexpcyc  11006  expnbnd  11025  expnlbnd  11026  remim  11545  imval2  11579  cjdivapi  11620  absdivapzi  11839  fprodge1  12325  ef01bndlem  12442  sin01gt0  12448  cos01gt0  12449  cos12dec  12454  absefib  12457  efieq1re  12458  zeo3  12554  evend2  12575  cnbl0  15399  reeff1olem  15636  sincosq1sgn  15691  sincosq3sgn  15693  sincosq4sgn  15694  rpelogb  15814  lgsdir2lem2  15902  konigsberglem5  16487