Theorem a1d 14

Description: Deduction introducing an embedded antecedent.

Naming convention: We often call a theorem a "deduction" and suffix its label with "d" whenever the hypotheses and conclusion are each prefixed with the same antecedent. This allows us to use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used; here ph would be replaced with a conjunction (df-an 198) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 7. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 3. In propositional calculus we usually prove the theorem form first without a suffix on its label (e.g. pm2.43 57 vs. pm2.43i 58 vs. pm2.43d 59), but (much) later we often suffix the theorem form's label with "t" as in negnegt 4157 vs. negneg 4154, especially when our "weak deduction theorem" dedth 1784 is used to prove the theorem form from its inference form. When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for somewhat misnamed "generalized") as in uniex 1947 vs. uniexg 1948.

Hypothesis

Ref	Expression
a1d.1	|- (ph -> ps)

Assertion

Ref	Expression
a1d	|- (ph -> (ch -> ps))

Proof of Theorem a1d

Step	Hyp	Ref	Expression
1		a1d.1	. . 3 |- (ph -> ps)
2	1	a1i 7	. 2 |- (ch -> (ph -> ps))
3	2	com12 13	1 |- (ph -> (ch -> ps))

Syntax hints:   -> wi 2

This theorem is referenced by:  syl3d 26  a1dd 42  mpid 48  pm2.21d 74  pm2.61d2 111  pm2.61iii 114  ja 118  pm2.48 230  pm3.4 266  adantr 306  adantld 307  adantlrl 314  adantrll 316  adantrrr 319  ibib 448  imbi2d 464  orbidi 510  tbt 541  biort 550  prlem1 576  eqvin.l1 851  hbsb4 905  ddelimf2 907  sbcom 916  ax11a 926  sbal1 996  mo 1020  moexex 1058  2eu1 1067  r19.22sdv 1279  r19.12 1281  birabsdv 1344  supsn 2168  dfwe2 2187  onfr 2237  ordunidif 2260  trsuc 2308  ordsucelsuc 2324  orduniorsuc 2337  limsuc 2361  limomss 2378  findsg 2398  tfinds 2401  tfindsg 2402  dmxp 2552  sotri 2630  fnun 2730  tz6.12-2 2845  ndmfv 2848  fveqres 2851  fvopabn 2873  cleqfv 2880  fvelrn 2883  isofrlem 2939  rdgsucopabn 2985  abianfplem 2999  abianfp 3000  ndmord 3064  oaordi 3148  oawordeulem 3156  breng 3280  brdomg 3281  f1oeng 3298  f1domg 3299  sdomdomtr 3370  ssenen 3399  onomeneq 3414  pssnn 3428  fiint 3445  inf3lem3 3466  infensuc 3484  r1ord 3499  rankr1 3518  r1pw 3529  r1pwcl 3530  scottex 3541  aceq5lem4 3561  aceq6b 3565  fodomb 3615  ondomon 3662  cardmin 3666  alephon 3671  alephcard 3673  alephnbtwn 3674  alephordi 3679  alephsucdom 3685  cflim 3704  cfsuc 3709  axextnd 3737  axrepnd 3740  axpowndlem3 3745  axpownd 3747  axregnd 3750  addnidpi 3822  ltexprlem7 3942  prlem936 3949  suplem1pr 3955  suppr 3957  mulgt0sr 4008  suppsr2 4017  suppsr3 4018  negeu 4124  receu 4215  add20 4329  nnind 4434  nn1suc 4435  nnleltp1t 4448  nnsub 4450  nndiv 4453  nominpos 4509  zaddclt 4590  zmulclt 4596  uzind 4603  qnegclt 4643  qbtwnre 4650  sqrlem6 4736  replimt 4798  clim0 4882  ruclem24 4908  infxpidmlem8 4940  infmap2 4953  hial2eqt 5060  hlim0 5140  occont 5168  chocuni 5179  occllem7 5186  hsupss 5310  spanss 5319  shlej1t 5356  orthin 5371  spansncol 5473  osumlem4 5533  mdbr2 5728  dmdbr2 5733  ssmd1 5734  ssmd2 5735  atcveq0 5746  chrelat2 5758  atexch 5769  atcvat4 5775  mdsymlem3 5778  mdsymlem4 5779  sumdmdlem 5786

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

metamath.org