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  2794  brelrn  4900  funpr  5311  fpm  6749  ener  6847  ltaddnq  7491  ltadd1sr  7860  map2psrprg  7889  mul02  8430  ltapi  8680  div0ap  8746  divclapzi  8791  divcanap1zi  8792  divcanap2zi  8793  divrecapzi  8794  divcanap3zi  8795  divcanap4zi  8796  divassapzi  8806  divmulapzi  8807  divdirapzi  8808  redivclapzi  8822  ltm1  8890  mulgt1  8907  recgt1i  8942  recreclt  8944  ltmul1i  8964  ltdiv1i  8965  ltmuldivi  8966  ltmul2i  8967  lemul1i  8968  lemul2i  8969  cju  9005  nnge1  9030  nngt0  9032  nnrecgt0  9045  elnnnn0c  9311  elnnz1  9366  recnz  9436  eluzsubi  9646  ge0gtmnf  9915  m1expcl2  10670  1exp  10677  m1expeven  10695  expubnd  10705  iexpcyc  10753  expnbnd  10772  expnlbnd  10773  remim  11042  imval2  11076  cjdivapi  11117  absdivapzi  11336  fprodge1  11821  ef01bndlem  11938  sin01gt0  11944  cos01gt0  11945  cos12dec  11950  absefib  11953  efieq1re  11954  zeo3  12050  evend2  12071  cnbl0  14854  reeff1olem  15091  sincosq1sgn  15146  sincosq3sgn  15148  sincosq4sgn  15149  rpelogb  15269  lgsdir2lem2  15354