Theorem mp3an12i 1382

Description: mp3an 1378 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 1368	. 2 |- ( th -> ta )
6	1, 5	syl 14	1 |- ( ch -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  funopsn  5891  map1  7101  exmidpw2en  7219  2omapen  7320  suplocsrlempr  8175  hashf1lem1  11301  geo2lim  12302  fprodge0  12423  fprodge1  12425  3dvds  12650  oddp1d2  12676  bezoutlema  12795  bezoutlemb  12796  pythagtriplem1  13067  exmidunben  13369  psrelbas  15151  psraddcl  15156  psrmulfval  15159  psrmulclfilem  15161  psr0cl  15163  psr0lid  15164  psrnegcl  15165  psrlinv  15166  psrgrp  15167  psr1clfi  15170  mplsubgfilemcl  15181  ismet  15536  isxmet  15537  dvidrelem  15884  coseq0negpitopi  16029  cosq34lt1  16043  cos02pilt1  16044  logdivlti  16075  1sgm2ppw  16250  ppiublem1  16252  bposlem6  16277  bposlem9  16280  lgseisenlem1  16355  lgseisen  16359  lgsquad3  16369  m1lgs  16370  pw1mapen  17192