Theorem mp3an12 1338

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 1335	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 424	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  mp3an12i  1352  ceqsralv  2791  brelrn  4895  funpr  5306  fpm  6735  ener  6833  ltaddnq  7467  ltadd1sr  7836  map2psrprg  7865  mul02  8406  ltapi  8655  div0ap  8721  divclapzi  8766  divcanap1zi  8767  divcanap2zi  8768  divrecapzi  8769  divcanap3zi  8770  divcanap4zi  8771  divassapzi  8781  divmulapzi  8782  divdirapzi  8783  redivclapzi  8797  ltm1  8865  mulgt1  8882  recgt1i  8917  recreclt  8919  ltmul1i  8939  ltdiv1i  8940  ltmuldivi  8941  ltmul2i  8942  lemul1i  8943  lemul2i  8944  cju  8980  nnge1  9005  nngt0  9007  nnrecgt0  9020  elnnnn0c  9285  elnnz1  9340  recnz  9410  eluzsubi  9620  ge0gtmnf  9889  m1expcl2  10632  1exp  10639  m1expeven  10657  expubnd  10667  iexpcyc  10715  expnbnd  10734  expnlbnd  10735  remim  11004  imval2  11038  cjdivapi  11079  absdivapzi  11298  fprodge1  11782  ef01bndlem  11899  sin01gt0  11905  cos01gt0  11906  cos12dec  11911  absefib  11914  efieq1re  11915  zeo3  12009  evend2  12030  cnbl0  14702  reeff1olem  14906  sincosq1sgn  14961  sincosq3sgn  14963  sincosq4sgn  14964  rpelogb  15081  lgsdir2lem2  15145