Theorem 3expia 1145

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

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

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 926

This theorem is referenced by:  mp3an3  1262  3gencl  2653  moi  2796  sotricim  4141  elirr  4347  en2lp  4360  suc11g  4363  3optocl  4504  sefvex  5310  f1oresrab  5447  ovmpt2s  5750  ov2gf  5751  poxp  5979  brtposg  6001  dfsmo2  6034  smoiun  6048  tfrlemibxssdm  6074  tfr1onlemsucfn  6087  tfr1onlemsucaccv  6088  tfr1onlembxssdm  6090  tfr1onlembfn  6091  tfr1onlemaccex  6095  tfr1onlemres  6096  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllembfn  6104  tfrcllemaccex  6108  tfrcllemres  6109  tfrcl  6111  nnsucsssuc  6235  nnaordi  6247  nnawordex  6267  mapvalg  6395  pmvalg  6396  elmapg  6398  xpdom3m  6530  ordiso  6708  pr2ne  6799  ltbtwnnqq  6953  prarloclem4  7036  addlocpr  7074  1idprl  7128  1idpru  7129  ltexprlemrnd  7143  recexprlemrnd  7167  recexprlem1ssl  7171  recexprlem1ssu  7172  recexprlemss1l  7173  recexprlemss1u  7174  aptisr  7303  axpre-apti  7399  ltxrlt  7531  axapti  7536  lttri3  7544  reapti  8032  apreap  8040  msqge0  8069  mulge0  8072  recexap  8096  mulap0b  8098  lt2msq  8319  zaddcl  8760  zdiv  8804  zextlt  8808  prime  8815  uzind2  8828  fzind  8831  lbzbi  9070  xltneg  9267  iocssre  9340  icossre  9341  iccssre  9342  fzen  9426  rebtwn2zlemshrink  9630  qbtwnxr  9634  ioo0  9636  ioom  9637  ico0  9638  ioc0  9639  expclzaplem  9944  expnegzap  9954  expaddzap  9964  expmulzap  9966  omgadd  10175  shftuz  10216  cau3lem  10512  climuni  10645  divalgb  11007  ndvdssub  11012  dvdsgcd  11083  lcmgcdlem  11141  qredeu  11161  isprm3  11182  prmdvdsexpr  11211  prmexpb  11212  bj-peano4  11496