Theorem 3impia 1178

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 1175	1 |- ( ( ph /\ ps /\ ch ) -> th )

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

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 964

This theorem is referenced by:  mopick2  2082  3gencl  2720  mob2  2864  moi  2867  reupick3  3361  disjne  3416  disji2  3922  tz7.2  4276  funopg  5157  fvun1  5487  fvopab6  5517  isores3  5716  ovmpt4g  5893  ovmpos  5894  ov2gf  5895  ofrval  5992  poxp  6129  smoel  6197  tfr1onlemaccex  6245  tfrcllemaccex  6258  nnaass  6381  qsel  6506  xpdom3m  6728  phpm  6759  ctssdc  6998  mkvprop  7032  prarloclem3  7305  aptisr  7587  axpre-apti  7693  axapti  7835  addn0nid  8136  divvalap  8434  letrp1  8606  p1le  8607  zextle  9142  zextlt  9143  btwnnz  9145  gtndiv  9146  uzind2  9163  fzind  9166  iccleub  9714  uzsubsubfz  9827  elfz0fzfz0  9903  difelfznle  9912  elfzo0le  9962  fzonmapblen  9964  fzofzim  9965  fzosplitprm1  10011  rebtwn2zlemstep  10030  qbtwnxr  10035  expcl2lemap  10305  expclzaplem  10317  expnegzap  10327  leexp2r  10347  expnbnd  10415  bcval4  10498  bccmpl  10500  absexpzap  10852  divalgb  11622  ndvdssub  11627  dvdsgcd  11700  dfgcd2  11702  rplpwr  11715  lcmgcdlem  11758  coprmdvds1  11772  qredeq  11777  prmdvdsexpr  11828  elrestr  12128  mopni  12651  sincosq1lem  12906