Theorem adantrr 395

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 373	. . 3 |- (ph -> (ps -> ch))
3	2	adantrd 391	. 2 |- (ph -> ((ps /\ th) -> ch))
4	3	imp 350	1 |- ((ph /\ (ps /\ th)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ad2ant2r 409  ad2ant2lr 410  anabss1 499  3ad2antr1 812  sbcom 1258  ax11eq 1363  ax11el 1364  ifboth 2375  po2nr 2847  sotric 2860  tz7.7 2973  ordsucun 3082  opelxp1 3205  isocnv 3896  isomin 3899  isoini 3900  oalim 4167  omlim 4168  oaass 4195  omordi 4197  omwordri 4203  odi 4210  oen0 4213  oewordri 4219  oeworde 4220  dom2d 4403  ssenen 4502  ssfi 4533  inf3lem6 4610  rankxplim3 4706  aceq5lem4 4730  aceq6b 4734  unidom 4800  axacndlem4 4954  ltapq 5068  ltmpq 5069  ltexpq 5072  ltexprlem6 5139  ssgt0sr 5209  add4t 5330  2addsubt 5381  mul4t 5412  muladdt 5413  xrlttrt 5545  ltleaddt 5637  rec11rt 5767  divdivdivt 5773  divdiv23t 5780  lemul2it 5827  lemul12ait 5830  ltmuldiv2t 5853  ltdivmult 5855  ltdivmul2t 5858  lemuldiv2t 5864  ltdiv23t 5880  lediv23t 5881  suprleub 6047  infmrcl 6057  xrsupsslem 6064  xrinfmsslem 6065  supxrunb1 6077  supxrunb2 6078  supxrleub 6087  zextltt 6178  zmax 6208  qbtwnre 6264  icounlem 6398  ioojoint 6402  recexpt 6581  expsubt 6584  expordit 6586  expord2t 6590  sqlecant 6627  lenegsqt 6870  seq1ublem 6896  fsumcom 7013  fsumshft 7016  2climnn 7087  2climnn0 7088  climge0 7097  climaddlem3 7101  climmullem1 7105  climmullem3 7107  climmullem5 7109  climmullem8 7112  climsqueeze 7125  climsqueeze2 7126  climcau 7141  serzf0 7154  ser1f0 7155  ser1cmp2 7162  cvgratlem2 7236  cvgratlem5 7239  fsum0diaglem2 7242  mulc1cncf 7264  acdc3lem 7471  acdclem 7479  infxpidmlem7 7543  infxpidmlem12 7548  eltg2t 7604  tgclt 7609  tgval3t 7610  tgss2t 7622  2basgent 7626  iscld 7654  ntrss 7673  ssnei2 7715  neindisj 7716  islp2 7732  cnpcl 7749  dnsconst 7773  ismsg 7785  blss 7838  blssex 7839  metcnp 7872  metcnpi3 7877  metcnpi4 7878  metcni2 7880  tgioolem 7899  lmss 7938  lmle 7945  metelcls 7950  metcnp4 7955  xplmi 7958  xpcn 7961  lmcau 7981  cmsss 7982  bcthlem11 7994  bcthlem15 7998  bcthlem18 8001  bcthlem19 8002  bcthlem20 8003  bcthlem21 8004  bcthlem24 8007  grpidinv 8037  grprcan 8048  grpinvid1 8057  grpinvid2 8058  grplcan 8060  abl4 8090  isring 8126  nvsubadd 8260  nvabs 8286  va1cnlem 8330  nvcnpi3 8407  nvcnpi4 8408  sspph 8500  ubthlem3 8516  ubthlem9 8522  ubthlem11 8524  ubthlem12 8525  ubthlem14 8527  hvadd4t 8890  hvaddsub4t 8930  chocuni 9157  occllem6 9163  shscl 9266  pjspansnt 9485  fh1t 9546  fh2t 9547  cm2jt 9548  spansncv 9582  5oalem2 9585  5oalem5 9588  5oalem6 9589  3oalem2 9593  hoadd4t 9695  cnvunopt 9827  bralnfnt 9857  eighmortht 9873  hmopst 9930  hmopmt 9931  hmopcot 9933  lnopcon 9948  lnfncon 9975  adjlnopt 10004  adjmult 10010  adjaddt 10011  nmopco 10013  kbass6t 10039  hstlet 10142  stles 10153  strlem3a 10164  hstrlem3a 10172  mdsl0 10222  mdexch 10247  atom1d 10265  superpos 10266  cvexchlem 10280  atoml 10294  atcvatlem 10297  irredlem2 10303  irredlem3 10304  atcvat4 10309  mdsymlem1 10315  mdsymlem3 10317  mdsymlem5 10319  mdsymlem6 10320  sumdmdlem 10330  sumdmdlem2 10331  cdj1 10345  cdj3lem2b 10349  nndivsub 10406

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

Copyright terms: Public domain