Theorem 3impia 1195

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

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

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 975

This theorem is referenced by:  mopick2  2102  3gencl  2764  mob2  2910  moi  2913  reupick3  3412  disjne  3468  disji2  3982  tz7.2  4339  funopg  5232  fvun1  5562  fvopab6  5592  isores3  5794  ovmpt4g  5975  ovmpos  5976  ov2gf  5977  ofrval  6071  poxp  6211  smoel  6279  tfr1onlemaccex  6327  tfrcllemaccex  6340  nnaass  6464  qsel  6590  xpdom3m  6812  phpm  6843  ctssdc  7090  mkvprop  7134  prarloclem3  7459  aptisr  7741  axpre-apti  7847  axapti  7990  addn0nid  8293  divvalap  8591  letrp1  8764  p1le  8765  zextle  9303  zextlt  9304  btwnnz  9306  gtndiv  9307  uzind2  9324  fzind  9327  iccleub  9888  uzsubsubfz  10003  elfz0fzfz0  10082  difelfznle  10091  elfzo0le  10141  fzonmapblen  10143  fzofzim  10144  fzosplitprm1  10190  rebtwn2zlemstep  10209  qbtwnxr  10214  icogelb  10222  expcl2lemap  10488  expclzaplem  10500  expnegzap  10510  leexp2r  10530  expnbnd  10599  bcval4  10686  bccmpl  10688  absexpzap  11044  divalgb  11884  ndvdssub  11889  dvdsgcd  11967  dfgcd2  11969  rplpwr  11982  nnmindc  11989  lcmgcdlem  12031  coprmdvds1  12045  qredeq  12050  prmdvdsexpr  12104  nnnn0modprm0  12209  pcexp  12263  difsqpwdvds  12291  prmpwdvds  12307  elrestr  12587  isnmgm  12614  grpasscan1  12762  grpinvnz  12770  mopni  13276  sincosq1lem  13540  logbgcd1irr  13679