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  2835  brelrn  4971  funpr  5389  fpm  6893  ener  6996  0fsupp  7223  ltaddnq  7687  ltadd1sr  8056  map2psrprg  8085  mul02  8625  ltapi  8875  div0ap  8941  divclapzi  8986  divcanap1zi  8987  divcanap2zi  8988  divrecapzi  8989  divcanap3zi  8990  divcanap4zi  8991  divassapzi  9001  divmulapzi  9002  divdirapzi  9003  redivclapzi  9017  ltm1  9085  mulgt1  9102  recgt1i  9137  recreclt  9139  ltmul1i  9159  ltdiv1i  9160  ltmuldivi  9161  ltmul2i  9162  lemul1i  9163  lemul2i  9164  cju  9200  nnge1  9225  nngt0  9227  nnrecgt0  9240  elnnnn0c  9506  elnnz1  9563  recnz  9634  eluzsubi  9845  ge0gtmnf  10119  m1expcl2  10886  1exp  10893  m1expeven  10911  expubnd  10921  iexpcyc  10969  expnbnd  10988  expnlbnd  10989  remim  11500  imval2  11534  cjdivapi  11575  absdivapzi  11794  fprodge1  12280  ef01bndlem  12397  sin01gt0  12403  cos01gt0  12404  cos12dec  12409  absefib  12412  efieq1re  12413  zeo3  12509  evend2  12530  cnbl0  15345  reeff1olem  15582  sincosq1sgn  15637  sincosq3sgn  15639  sincosq4sgn  15640  rpelogb  15760  lgsdir2lem2  15848  konigsberglem5  16433