Theorem 3expib 1070

Description: Exportation from triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 1066	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp3a 388	1 |- (ph -> ((ps /\ ch) -> th))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  vtocl3ga 2354  fco 4573  fvco2 4737  onfununi 5116  3ecoptocl 5364  fodomfib 5657  icoshft 7577  fzen 7664  ser1add2i 7751  iserzmulc1 8396  mulc1cncf 8541  ivthlem6 8548  ivthlem7 8549  mettri4 9091  opnin 9146  opntop 9147  tgbl 9148  blbas 9149  grpdivf 9370  ipf 9705  sspival 9736  spwmo 9999  spwval 10002  pilem1 10020  sincosq1sgn 10053  sincosq2sgn 10054  sincosq3sgn 10055  sincosq4sgn 10056  efifolem4 10079  efifolem5 10080  hausnei2 10222  filintf 10274  filfbas 10276  fsubbas 10281  neifil 10302  hausfillim 10303  flimopn 10321  shintcli 10926  adjadj 11497  unopadj2 11499  hmopadj 11500  bnj1200 12977  bnj1381 13098  bnj594 13300  bnj580 13301  bnj600 13308  bnj1321 13498  bnj1367 13511  ghomf1olem 13637  algcvga 13747  dvdsgcd 13765  cur1vald 14547  curgrpact 14735  addvecom 14809  invaddvec 14810  svli2 14826  truni2 14850  inttop2 14863  homcard 14893  qusp 14908  conttnf 14944  bsi2 14992  intrn 14994  lvsovso 15038  dualcat2lem 15129  dualded 15132  dualcat2 15133  mrdmcd 15143  cmpassoh 15150  imonclem 15162  ismonc 15163  cmpmon 15164  icmpmon 15165  iepiclem 15172  isepic 15173  idfisf 15189  isline1 15294  elfiun 15369  fitop 15401  fness 15491  locfincomp 15514  topmtcl 15525  ist1-2 15542  ist1-3 15543  filssufillem 15570  filcon 15580  fmfnfmlem4 15597  filnetlem4 15643  neificl 15841  metf1o 15843  haustlmu 15906  heiborlem29 15983  rrnmet 16016  abl4pnp 16037  divrngcl 16110  keridl 16180  prnc 16215  linepsub 17232  pmapsub 17250

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain