Theorem mp3an12 1340

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  mp3an12i  1354  ceqsralv  2808  brelrn  4930  funpr  5345  fpm  6791  ener  6894  ltaddnq  7555  ltadd1sr  7924  map2psrprg  7953  mul02  8494  ltapi  8744  div0ap  8810  divclapzi  8855  divcanap1zi  8856  divcanap2zi  8857  divrecapzi  8858  divcanap3zi  8859  divcanap4zi  8860  divassapzi  8870  divmulapzi  8871  divdirapzi  8872  redivclapzi  8886  ltm1  8954  mulgt1  8971  recgt1i  9006  recreclt  9008  ltmul1i  9028  ltdiv1i  9029  ltmuldivi  9030  ltmul2i  9031  lemul1i  9032  lemul2i  9033  cju  9069  nnge1  9094  nngt0  9096  nnrecgt0  9109  elnnnn0c  9375  elnnz1  9430  recnz  9501  eluzsubi  9711  ge0gtmnf  9980  m1expcl2  10743  1exp  10750  m1expeven  10768  expubnd  10778  iexpcyc  10826  expnbnd  10845  expnlbnd  10846  remim  11286  imval2  11320  cjdivapi  11361  absdivapzi  11580  fprodge1  12065  ef01bndlem  12182  sin01gt0  12188  cos01gt0  12189  cos12dec  12194  absefib  12197  efieq1re  12198  zeo3  12294  evend2  12315  cnbl0  15121  reeff1olem  15358  sincosq1sgn  15413  sincosq3sgn  15415  sincosq4sgn  15416  rpelogb  15536  lgsdir2lem2  15621