Theorem 3impia 1190

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impia.1	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Assertion

Ref	Expression
3impia	|- ( ( ph /\ ps /\ ch ) -> th )

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 |- ( ( ph /\ ps ) -> ( ch -> th ) )
2	1	ex 114	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1183	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

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 970

This theorem is referenced by:  mopick2  2097  3gencl  2760  mob2  2906  moi  2909  reupick3  3407  disjne  3462  disji2  3975  tz7.2  4332  funopg  5222  fvun1  5552  fvopab6  5582  isores3  5783  ovmpt4g  5964  ovmpos  5965  ov2gf  5966  ofrval  6060  poxp  6200  smoel  6268  tfr1onlemaccex  6316  tfrcllemaccex  6329  nnaass  6453  qsel  6578  xpdom3m  6800  phpm  6831  ctssdc  7078  mkvprop  7122  prarloclem3  7438  aptisr  7720  axpre-apti  7826  axapti  7969  addn0nid  8272  divvalap  8570  letrp1  8743  p1le  8744  zextle  9282  zextlt  9283  btwnnz  9285  gtndiv  9286  uzind2  9303  fzind  9306  iccleub  9867  uzsubsubfz  9982  elfz0fzfz0  10061  difelfznle  10070  elfzo0le  10120  fzonmapblen  10122  fzofzim  10123  fzosplitprm1  10169  rebtwn2zlemstep  10188  qbtwnxr  10193  icogelb  10201  expcl2lemap  10467  expclzaplem  10479  expnegzap  10489  leexp2r  10509  expnbnd  10578  bcval4  10665  bccmpl  10667  absexpzap  11022  divalgb  11862  ndvdssub  11867  dvdsgcd  11945  dfgcd2  11947  rplpwr  11960  nnmindc  11967  lcmgcdlem  12009  coprmdvds1  12023  qredeq  12028  prmdvdsexpr  12082  nnnn0modprm0  12187  pcexp  12241  difsqpwdvds  12269  prmpwdvds  12285  elrestr  12564  isnmgm  12591  mopni  13122  sincosq1lem  13386  logbgcd1irr  13525