Theorem mp3an12 1327

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  mp3an12i  1341  ceqsralv  2768  brelrn  4860  funpr  5268  fpm  6680  ener  6778  ltaddnq  7405  ltadd1sr  7774  map2psrprg  7803  mul02  8343  ltapi  8592  div0ap  8658  divclapzi  8703  divcanap1zi  8704  divcanap2zi  8705  divrecapzi  8706  divcanap3zi  8707  divcanap4zi  8708  divassapzi  8718  divmulapzi  8719  divdirapzi  8720  redivclapzi  8734  ltm1  8802  mulgt1  8819  recgt1i  8854  recreclt  8856  ltmul1i  8876  ltdiv1i  8877  ltmuldivi  8878  ltmul2i  8879  lemul1i  8880  lemul2i  8881  cju  8917  nnge1  8941  nngt0  8943  nnrecgt0  8956  elnnnn0c  9220  elnnz1  9275  recnz  9345  eluzsubi  9554  ge0gtmnf  9822  m1expcl2  10541  1exp  10548  m1expeven  10566  expubnd  10576  iexpcyc  10624  expnbnd  10643  expnlbnd  10644  remim  10868  imval2  10902  cjdivapi  10943  absdivapzi  11162  fprodge1  11646  ef01bndlem  11763  sin01gt0  11768  cos01gt0  11769  cos12dec  11774  absefib  11777  efieq1re  11778  zeo3  11872  evend2  11893  cnbl0  14004  reeff1olem  14162  sincosq1sgn  14217  sincosq3sgn  14219  sincosq4sgn  14220  rpelogb  14337  lgsdir2lem2  14400