Theorem 3expia 1194

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

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

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 969

This theorem is referenced by:  mp3an3  1315  3gencl  2755  moi  2904  sotricim  4295  elirr  4512  en2lp  4525  suc11g  4528  3optocl  4676  sefvex  5501  f1oresrab  5644  ovmpos  5956  ov2gf  5957  poxp  6191  brtposg  6213  dfsmo2  6246  smoiun  6260  tfrlemibxssdm  6286  tfr1onlemsucfn  6299  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfr1onlemaccex  6307  tfr1onlemres  6308  tfrcllemsucfn  6312  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllembfn  6316  tfrcllemaccex  6320  tfrcllemres  6321  tfrcl  6323  nnsucsssuc  6451  nnaordi  6467  nnawordex  6487  mapvalg  6615  pmvalg  6616  elmapg  6618  xpdom3m  6791  ordiso  6992  ctssdc  7069  pr2ne  7139  ltbtwnnqq  7347  prarloclem4  7430  addlocpr  7468  1idprl  7522  1idpru  7523  ltexprlemrnd  7537  recexprlemrnd  7561  recexprlem1ssl  7565  recexprlem1ssu  7566  recexprlemss1l  7567  recexprlemss1u  7568  aptisr  7711  axpre-apti  7817  ltxrlt  7955  axapti  7960  lttri3  7969  reapti  8468  apreap  8476  msqge0  8505  mulge0  8508  recexap  8541  mulap0b  8543  lt2msq  8772  zaddcl  9222  zdiv  9270  zextlt  9274  prime  9281  uzind2  9294  fzind  9297  lbzbi  9545  xltneg  9763  xlt2add  9807  iocssre  9880  icossre  9881  iccssre  9882  fzen  9968  rebtwn2zlemshrink  10179  qbtwnxr  10183  ioo0  10185  ioom  10186  ico0  10187  ioc0  10188  expclzaplem  10469  expnegzap  10479  expaddzap  10489  expmulzap  10491  omgadd  10704  shftuz  10745  cau3lem  11042  climuni  11220  efltim  11625  divalgb  11847  ndvdssub  11852  dvdsgcd  11930  lcmgcdlem  11988  qredeu  12008  isprm3  12029  prmdvdsexpr  12059  prmexpb  12060  fermltl  12143  coprimeprodsq  12166  pythagtrip  12192  pcpremul  12202  pcdvdsb  12228  pc2dvds  12238  ctinf  12300  cnntr  12766  cncnp2m  12772  cnptoprest  12780  lmtopcnp  12791  cnmptcom  12839  hmeof1o  12850  blpnf  12941  blssps  12968  blss  12969  blssec  12979  neibl  13032  climcncf  13112  cnplimcim  13177  bj-peano4  13672  triap  13742