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  2847  brelrn  4995  funpr  5413  fpm  6928  ener  7032  0fsupp  7264  ltaddnq  7738  ltadd1sr  8107  map2psrprg  8136  mul02  8677  ltapi  8927  div0ap  8993  divclapzi  9038  divcanap1zi  9039  divcanap2zi  9040  divrecapzi  9041  divcanap3zi  9042  divcanap4zi  9043  divassapzi  9053  divmulapzi  9054  divdirapzi  9055  redivclapzi  9069  ltm1  9137  mulgt1  9154  recgt1i  9189  recreclt  9191  ltmul1i  9211  ltdiv1i  9212  ltmuldivi  9213  ltmul2i  9214  lemul1i  9215  lemul2i  9216  cju  9252  nnge1  9277  nngt0  9279  nnrecgt0  9292  elnnnn0c  9558  elnnz1  9617  recnz  9689  eluzsubi  9900  ge0gtmnf  10175  m1expcl2  10947  1exp  10954  m1expeven  10972  expubnd  10982  iexpcyc  11030  resq01  11044  expnbnd  11050  expnlbnd  11051  remim  11570  imval2  11604  cjdivapi  11645  absdivapzi  11864  fprodge1  12350  ef01bndlem  12467  sin01gt0  12473  cos01gt0  12474  cos12dec  12479  absefib  12482  efieq1re  12483  zeo3  12579  evend2  12600  cnbl0  15525  reeff1olem  15762  sincosq1sgn  15817  sincosq3sgn  15819  sincosq4sgn  15820  rpelogb  15940  lgsdir2lem2  16028  konigsberglem5  16613