Theorem 3expia 1166

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

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

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  mp3an3  1287  3gencl  2691  moi  2836  sotricim  4205  elirr  4416  en2lp  4429  suc11g  4432  3optocl  4577  sefvex  5396  f1oresrab  5539  ovmpos  5848  ov2gf  5849  poxp  6083  brtposg  6105  dfsmo2  6138  smoiun  6152  tfrlemibxssdm  6178  tfr1onlemsucfn  6191  tfr1onlemsucaccv  6192  tfr1onlembxssdm  6194  tfr1onlembfn  6195  tfr1onlemaccex  6199  tfr1onlemres  6200  tfrcllemsucfn  6204  tfrcllemsucaccv  6205  tfrcllembxssdm  6207  tfrcllembfn  6208  tfrcllemaccex  6212  tfrcllemres  6213  tfrcl  6215  nnsucsssuc  6342  nnaordi  6358  nnawordex  6378  mapvalg  6506  pmvalg  6507  elmapg  6509  xpdom3m  6681  ordiso  6873  ctssdc  6950  pr2ne  6998  ltbtwnnqq  7171  prarloclem4  7254  addlocpr  7292  1idprl  7346  1idpru  7347  ltexprlemrnd  7361  recexprlemrnd  7385  recexprlem1ssl  7389  recexprlem1ssu  7390  recexprlemss1l  7391  recexprlemss1u  7392  aptisr  7521  axpre-apti  7620  ltxrlt  7754  axapti  7759  lttri3  7767  reapti  8259  apreap  8267  msqge0  8296  mulge0  8299  recexap  8327  mulap0b  8329  lt2msq  8554  zaddcl  8998  zdiv  9043  zextlt  9047  prime  9054  uzind2  9067  fzind  9070  lbzbi  9310  xltneg  9512  xlt2add  9556  iocssre  9629  icossre  9630  iccssre  9631  fzen  9716  rebtwn2zlemshrink  9924  qbtwnxr  9928  ioo0  9930  ioom  9931  ico0  9932  ioc0  9933  expclzaplem  10210  expnegzap  10220  expaddzap  10230  expmulzap  10232  omgadd  10441  shftuz  10482  cau3lem  10778  climuni  10954  efltim  11255  divalgb  11470  ndvdssub  11475  dvdsgcd  11546  lcmgcdlem  11604  qredeu  11624  isprm3  11645  prmdvdsexpr  11674  prmexpb  11675  ctinf  11788  cnntr  12236  cncnp2m  12242  cnptoprest  12250  lmtopcnp  12261  cnmptcom  12309  blpnf  12389  blssps  12416  blss  12417  blssec  12427  neibl  12480  climcncf  12557  cnplimcim  12592  bj-peano4  12845  triap  12916