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  7493  ltadd1sr  7862  map2psrprg  7891  mul02  8432  ltapi  8682  div0ap  8748  divclapzi  8793  divcanap1zi  8794  divcanap2zi  8795  divrecapzi  8796  divcanap3zi  8797  divcanap4zi  8798  divassapzi  8808  divmulapzi  8809  divdirapzi  8810  redivclapzi  8824  ltm1  8892  mulgt1  8909  recgt1i  8944  recreclt  8946  ltmul1i  8966  ltdiv1i  8967  ltmuldivi  8968  ltmul2i  8969  lemul1i  8970  lemul2i  8971  cju  9007  nnge1  9032  nngt0  9034  nnrecgt0  9047  elnnnn0c  9313  elnnz1  9368  recnz  9438  eluzsubi  9648  ge0gtmnf  9917  m1expcl2  10672  1exp  10679  m1expeven  10697  expubnd  10707  iexpcyc  10755  expnbnd  10774  expnlbnd  10775  remim  11044  imval2  11078  cjdivapi  11119  absdivapzi  11338  fprodge1  11823  ef01bndlem  11940  sin01gt0  11946  cos01gt0  11947  cos12dec  11952  absefib  11955  efieq1re  11956  zeo3  12052  evend2  12073  cnbl0  14878  reeff1olem  15115  sincosq1sgn  15170  sincosq3sgn  15172  sincosq4sgn  15173  rpelogb  15293  lgsdir2lem2  15378