Theorem mp3an12i 1378

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

Hypotheses

Ref	Expression
mp3an12i.1	|- ph
mp3an12i.2	|- ps
mp3an12i.3	|- ( ch -> th )
mp3an12i.4	|- ( ( ph /\ ps /\ th ) -> ta )

Assertion

Ref	Expression
mp3an12i	|- ( ch -> ta )

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 |- ( ch -> th )
2		mp3an12i.1	. . 3 |- ph
3		mp3an12i.2	. . 3 |- ps
4		mp3an12i.4	. . 3 |- ( ( ph /\ ps /\ th ) -> ta )
5	2, 3, 4	mp3an12 1364	. 2 |- ( th -> ta )
6	1, 5	syl 14	1 |- ( ch -> ta )

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  funopsn  5838  map1  7030  exmidpw2en  7147  suplocsrlempr  8087  geo2lim  12157  fprodge0  12278  fprodge1  12280  3dvds  12505  oddp1d2  12531  bezoutlema  12650  bezoutlemb  12651  pythagtriplem1  12918  exmidunben  13127  psrelbas  14776  psraddcl  14781  psr0cl  14782  psr0lid  14783  psrnegcl  14784  psrlinv  14785  psrgrp  14786  psr1clfi  14789  mplsubgfilemcl  14800  ismet  15155  isxmet  15156  dvidrelem  15503  coseq0negpitopi  15647  cosq34lt1  15661  cos02pilt1  15662  logdivlti  15692  1sgm2ppw  15809  lgseisenlem1  15889  lgseisen  15893  lgsquad3  15903  m1lgs  15904  2omapen  16716  pw1mapen  16718