Theorem 3expia 1195

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1192	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 123	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:  mp3an3  1316  3gencl  2760  moi  2909  sotricim  4301  elirr  4518  en2lp  4531  suc11g  4534  3optocl  4682  sefvex  5507  f1oresrab  5650  ovmpos  5965  ov2gf  5966  poxp  6200  brtposg  6222  dfsmo2  6255  smoiun  6269  tfrlemibxssdm  6295  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemaccex  6329  tfrcllemres  6330  tfrcl  6332  nnsucsssuc  6460  nnaordi  6476  nnawordex  6496  mapvalg  6624  pmvalg  6625  elmapg  6627  xpdom3m  6800  ordiso  7001  ctssdc  7078  pr2ne  7148  ltbtwnnqq  7356  prarloclem4  7439  addlocpr  7477  1idprl  7531  1idpru  7532  ltexprlemrnd  7546  recexprlemrnd  7570  recexprlem1ssl  7574  recexprlem1ssu  7575  recexprlemss1l  7576  recexprlemss1u  7577  aptisr  7720  axpre-apti  7826  ltxrlt  7964  axapti  7969  lttri3  7978  reapti  8477  apreap  8485  msqge0  8514  mulge0  8517  recexap  8550  mulap0b  8552  lt2msq  8781  zaddcl  9231  zdiv  9279  zextlt  9283  prime  9290  uzind2  9303  fzind  9306  lbzbi  9554  xltneg  9772  xlt2add  9816  iocssre  9889  icossre  9890  iccssre  9891  fzen  9978  rebtwn2zlemshrink  10189  qbtwnxr  10193  ioo0  10195  ioom  10196  ico0  10197  ioc0  10198  expclzaplem  10479  expnegzap  10489  expaddzap  10499  expmulzap  10501  omgadd  10715  shftuz  10759  cau3lem  11056  climuni  11234  efltim  11639  divalgb  11862  ndvdssub  11867  dvdsgcd  11945  lcmgcdlem  12009  qredeu  12029  isprm3  12050  prmdvdsexpr  12082  prmexpb  12083  fermltl  12166  coprimeprodsq  12189  pythagtrip  12215  pcpremul  12225  pcdvdsb  12251  pc2dvds  12261  ctinf  12363  cnntr  12865  cncnp2m  12871  cnptoprest  12879  lmtopcnp  12890  cnmptcom  12938  hmeof1o  12949  blpnf  13040  blssps  13067  blss  13068  blssec  13078  neibl  13131  climcncf  13211  cnplimcim  13276  bj-peano4  13837  triap  13908