Theorem 3impia 830

Description: Importation to triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 |- ((ph /\ ps) -> (ch -> th))
2	1	ex 373	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 827	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  3gencl 1830  vtoclegft 1856  disjne 2315  opthgg 2789  tz7.2 2931  brelrng 3343  ndmoprg 4043  oaass 4195  xpdom1g 4444  unidomg 4809  axsup 5507  ltnet 5516  xrltnet 5565  divclt 5712  divcan1t 5724  divcan1tOLD 5725  divcan2tOLD 5727  divrect 5739  divcan3t 5760  divcan3tOLD 5761  redivclt 5800  letrp1t 5816  p1let 5817  zextlet 6189  zextltt 6190  btwnnzt 6192  gtndivt 6193  uzind2 6206  flwordit 6237  ceilet 6250  qbtwnre 6278  qbtwnxr 6279  snunioo 6415  elfz4t 6475  expge1t 6593  exple1t 6607  absdivt 6860  cjdivt 6889  bccl2t 6971  fsum1ps 7018  iserzext 7135  isumreclt 7210  cncffvelrnOLD 7267  ivthlem6 7286  ivthlem7 7287  znnenlem 7501  clsndisj 7706  metcni 7894  lmfss 7948  lmcl 7949  bcthlem8 8006  bcth 8032  grpasscan1 8077  grplactf1o 8098  nvs 8290  nvtri 8298  nmlno0 8455  nmlnoubi 8456  hlipgt0 8616  spwnex 8661  sincosq1lem 8703  efifolem4 8725  efifolem5 8726  ocnelt 9170  elspansn2t 9490  elspansn3t 9495  normcant 9499  pjoml2t 9554  lecmt 9560  osumt 9588  nmbdfnlbt 9979  leopmult 10067  hstpytht 10156  cvnbtwnt 10213  ssmd1 10238  ssmd2 10239  ssdmd1 10240  ssdmd2 10241  cvmdt 10263  cvdmdt 10264  superpos 10281  cayleylem2 10410  cnvhmphb 10526  dmse1 10623  mslb1 10629  2wsms 10630  cmpassoh 10729  cmpmon 10743  icmpmon 10744

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 147  df-an 225  df-3an 777

Copyright terms: Public domain