Theorem 3impia 1135

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 113	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1132	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  mopick2  2024  3gencl  2633  mob2  2772  moi  2775  reupick3  3249  disjne  3297  tz7.2  4109  funopg  4954  fvun1  5260  fvopab6  5285  isores3  5475  ovmpt4g  5643  ovmpt2s  5644  ov2gf  5645  ofrval  5742  poxp  5873  smoel  5938  nnaass  6087  qsel  6206  xpdom3m  6331  phpm  6351  prarloclem3  6687  aptisr  6955  axpre-apti  7051  axapti  7183  addn0nid  7478  divvalap  7762  letrp1  7926  p1le  7927  zextle  8438  zextlt  8439  btwnnz  8441  gtndiv  8442  uzind2  8459  fzind  8462  iccleub  8954  uzsubsubfz  9066  elfz0fzfz0  9137  difelfznle  9146  elfzo0le  9194  fzonmapblen  9196  fzofzim  9197  fzosplitprm1  9243  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  qbtwnxr  9266  expcl2lemap  9488  expclzaplem  9500  expnegzap  9510  leexp2r  9530  expnbnd  9596  bcval4  9679  bccmpl  9681  absexpzap  9966  divalgb  10325  ndvdssub  10330  dvdsgcd  10401  dfgcd2  10403  rplpwr  10416  lcmgcdlem  10459  coprmdvds1  10473  qredeq  10478  prmdvdsexpr  10529