Theorem adantlrl 434

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

Ref	Expression
adantlrl	|- (((ph /\ (ta /\ ps)) /\ ch) -> th)

Proof of Theorem adantlrl

Step	Hyp	Ref	Expression
1		adantl2.1	. . . 4 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 407	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	a1d 15	. 2 |- (ph -> (ta -> (ps -> (ch -> th))))
4	3	imp42 396	1 |- (((ph /\ (ta /\ ps)) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  omlimcl 5257  odi 5258  oelim2 5270  prlem936b 6306  qbtwnre 7459  bccl2 8223  acdc3lem 8754  acdclem 8763  txbas 8933  metequiv 9158  metcnp 9165  metcnp3 9174  xplmi 9251  bcthlem27 9303  bcthlem28 9304  grprcan 9347  minveclem30 9919  minveclem31 9920  uptx 10226  filrn 10293  hausfillim 10303  cncomp 10331  unoplin 11481  hmoplin 11503  nlelchi 11631  superpos 11926  cnsubsp 15426  cnconn 15444  topfneec 15501  ufileu 15573  fzsplit 15792  fdc 15812  geomcau 15849  cnss 15892  sstotbnd 15936  isbnd3 15941  ismtyres 15954  rrncms 16019  rrntotbnd 16022  phtpycolem5 16055  pcohtpylem3 16082  isdivrng2 16111  rnghomco 16128  rngisocnv 16135  grprcanNEW 17122

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

Copyright terms: Public domain