Theorem mp3an12 1306

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

Syntax hints:   → wi 4   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  mp3an12i  1320  ceqsralv  2720  brelrn  4780  funpr  5183  fpm  6583  ener  6681  ltaddnq  7239  ltadd1sr  7608  map2psrprg  7637  mul02  8173  ltapi  8422  div0ap  8486  divclapzi  8531  divcanap1zi  8532  divcanap2zi  8533  divrecapzi  8534  divcanap3zi  8535  divcanap4zi  8536  divassapzi  8546  divmulapzi  8547  divdirapzi  8548  redivclapzi  8562  ltm1  8628  mulgt1  8645  recgt1i  8680  recreclt  8682  ltmul1i  8702  ltdiv1i  8703  ltmuldivi  8704  ltmul2i  8705  lemul1i  8706  lemul2i  8707  cju  8743  nnge1  8767  nngt0  8769  nnrecgt0  8782  elnnnn0c  9046  elnnz1  9101  recnz  9168  eluzsubi  9377  ge0gtmnf  9636  m1expcl2  10346  1exp  10353  m1expeven  10371  expubnd  10381  iexpcyc  10428  expnbnd  10446  expnlbnd  10447  remim  10664  imval2  10698  cjdivapi  10739  absdivapzi  10958  ef01bndlem  11499  sin01gt0  11504  cos01gt0  11505  cos12dec  11510  absefib  11513  efieq1re  11514  zeo3  11601  evend2  11622  cnbl0  12742  reeff1olem  12900  sincosq1sgn  12955  sincosq3sgn  12957  sincosq4sgn  12958  rpelogb  13074