Theorem mp3an12i 1352

Description: mp3an 1348 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an12i.1	⊢ 𝜑
mp3an12i.2	⊢ 𝜓
mp3an12i.3	⊢ (𝜒 → 𝜃)
mp3an12i.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
mp3an12i	⊢ (𝜒 → 𝜏)

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 ⊢ (𝜒 → 𝜃)
2		mp3an12i.1	. . 3 ⊢ 𝜑
3		mp3an12i.2	. . 3 ⊢ 𝜓
4		mp3an12i.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	mp3an12 1338	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 14	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:  map1  6880  exmidpw2en  6982  suplocsrlempr  7893  geo2lim  11700  fprodge0  11821  fprodge1  11823  3dvds  12048  oddp1d2  12074  bezoutlema  12193  bezoutlemb  12194  pythagtriplem1  12461  exmidunben  12670  psrelbas  14309  psraddcl  14314  psr0cl  14315  psr0lid  14316  psrnegcl  14317  psrlinv  14318  psrgrp  14319  psr1clfi  14322  mplsubgfilemcl  14333  ismet  14688  isxmet  14689  dvidrelem  15036  coseq0negpitopi  15180  cosq34lt1  15194  cos02pilt1  15195  logdivlti  15225  1sgm2ppw  15339  lgseisenlem1  15419  lgseisen  15423  lgsquad3  15433  m1lgs  15434  2omapen  15751