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  5860  map1  7054  exmidpw2en  7172  2omapen  7270  suplocsrlempr  8122  geo2lim  12202  fprodge0  12323  fprodge1  12325  3dvds  12550  oddp1d2  12576  bezoutlema  12695  bezoutlemb  12696  pythagtriplem1  12963  exmidunben  13177  psrelbas  14830  psraddcl  14835  psr0cl  14836  psr0lid  14837  psrnegcl  14838  psrlinv  14839  psrgrp  14840  psr1clfi  14843  mplsubgfilemcl  14854  ismet  15209  isxmet  15210  dvidrelem  15557  coseq0negpitopi  15701  cosq34lt1  15715  cos02pilt1  15716  logdivlti  15746  1sgm2ppw  15863  lgseisenlem1  15943  lgseisen  15947  lgsquad3  15957  m1lgs  15958  pw1mapen  16770