Theorem 3impib 1262

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 452	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1256	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  mob  3388  eqreu  3398  dedth3h  4141  prproe  4434  rbropap  5016  breldmg  5330  ssimaexg  6264  funopdmsn  6415  wfr3g  7413  dfsmo2  7444  omwordri  7652  3ecoptocl  7839  cfslb  9088  cofsmo  9091  cfsmolem  9092  coftr  9095  domtriomlem  9264  zorn2lem7  9324  ttukey2g  9338  gchi  9446  tskxpss  9594  tskord  9602  infm3  10982  uzind  11469  fzind  11475  fnn0ind  11476  xltnegi  12047  axdc4uz  12783  facwordi  13076  swrdnd2  13433  cshwidxmod  13549  relexpsucr  13769  relexpsucl  13773  relexprelg  13778  relexpaddnn  13791  caubnd  14098  mulgcd  15265  lcmfdvds  15355  lcmfdvdsb  15356  coprmdvds1  15365  pcfac  15603  ramz  15729  imasleval  16201  cictr  16465  initoeu2lem1  16664  drsdir  16935  psasym  17210  pstr  17211  tsrlin  17219  dirge  17237  mgmcl  17245  mhmlin  17342  mhmmulg  17583  issubg2  17609  nsgbi  17625  cygabl  18292  gsumcom2  18374  srgmulgass  18531  dvdsrtr  18652  drnginvrcl  18764  drnginvrn0  18765  drnginvrl  18766  drnginvrr  18767  isdrngd  18772  issubrg2  18800  abvmul  18829  abvtri  18830  lmhmlin  19035  domnmuln0  19298  ipcj  19979  cssincl  20032  obsip  20065  decpmatmulsumfsupp  20578  mp2pm2mplem4  20614  pm2mpghm  20621  pm2mpmhmlem1  20623  inopn  20704  basis1  20754  iscldtop  20899  2ndcdisj  21259  cnmpt2t  21476  cnmpt22  21477  cnmptcom  21481  fbasssin  21640  ptcmplem3  21858  xmeteq0  22143  prdsxmslem2  22334  nmvs  22480  nmolb  22521  volfiniun  23315  sincosq1sgn  24250  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  ewlkle  26501  wwlksnext  26788  umgr2adedgwlklem  26840  elwwlks2ons3  26848  umgrwwlks2on  26850  wwlksext2clwwlk  26924  clwlksfclwwlk  26962  conngrv2edg  27055  frgrwopregasn  27180  frgrwopregbsn  27181  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  frgr2wwlkeu  27191  ablocom  27402  nmcvcn  27550  ipassi  27696  htth  27775  shaddcl  28074  shmulcl  28075  shsubcl  28077  chlimi  28091  pjspansn  28436  cnopc  28772  cnfnc  28789  adj1  28792  lnfnmul  28907  atord  29247  atcvat2  29248  cdj3i  29300  nexple  30071  signstfvc  30651  bnj910  31018  bnj1154  31067  pconncn  31206  mrsubccat  31415  shftvalg  31617  frr3g  31779  linethru  32260  sin2h  33399  cos2h  33400  tan2h  33401  dvasin  33496  areacirclem1  33500  riotasv  34245  lsmsatcv  34297  omllaw  34530  2llnjN  34853  dalawlem10  35166  dalawlem13  35169  dalawlem14  35170  pclfinclN  35236  ismrc  37264  fzsplit1nn0  37317  pell1234qrmulcl  37419  pell14qrmulcl  37427  iunrelexp0  37994  bi23impib  38691  bi13impib  38692  trelded  38781  suctrALT  39061  suctrALTcf  39158  suctrALTcfVD  39159  stoweidlem17  40234  zm1nn  41316  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgblthelfgott  41703  tgblthelfgottOLD  41709  mgmhmlin  41786  issubmgm2  41790  clcllaw  41827  rnghmmul  41900  ztprmneprm  42125  lcoel0  42217  linindslinci  42237