![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > a1dd | Structured version Visualization version GIF version |
Description: Double deduction introducing an antecedent. Deduction associated with a1d 25. Double deduction associated with ax-1 6 and a1i 11. (Contributed by NM, 17-Dec-2004.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.) |
Ref | Expression |
---|---|
a1dd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
a1dd | ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a1dd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | ax-1 6 | . 2 ⊢ (𝜒 → (𝜃 → 𝜒)) | |
3 | 1, 2 | syl6 35 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: 2a1dd 51 merco2 1739 equvel 2455 propeqop 5469 funopsn 7099 xpexr 7860 omordi 8518 omwordi 8523 odi 8531 omass 8532 oen0 8538 oewordi 8543 oewordri 8544 nnmwordi 8587 omabs 8602 fisupg 9242 fiinfg 9442 cantnfle 9614 cantnflem1 9632 pr2neOLD 9948 gchina 10642 nqereu 10872 supsrlem 11054 1re 11162 lemul1a 12016 xlemul1a 13214 xrsupsslem 13233 xrinfmsslem 13234 xrub 13238 supxrunb1 13245 supxrunb2 13246 difelfzle 13561 addmodlteq 13858 seqcl2 13933 facdiv 14194 facwordi 14196 faclbnd 14197 pfxccat3 14629 dvdsabseq 16202 divgcdcoprm0 16548 2mulprm 16576 exprmfct 16587 prmfac1 16604 pockthg 16785 cply1mul 21681 mdetralt 21973 cmpsub 22767 fbfinnfr 23208 alexsubALTlem2 23415 alexsubALTlem3 23416 ovolicc2lem3 24899 fta1g 25548 fta1 25684 mulcxp 26056 cxpcn3lem 26116 gausslemma2dlem4 26733 colinearalg 27901 upgrwlkdvdelem 28726 umgr2wlk 28936 clwwlknwwlksn 29024 clwwlknonex2lem2 29094 dmdbr5ati 31406 cvmlift3lem4 33956 dfon2lem9 34405 fscgr 34694 colinbtwnle 34732 broutsideof2 34736 a1i14 34801 a1i24 34802 ordcmp 34948 bj-peircestab 35045 wl-aleq 36023 itg2addnc 36161 filbcmb 36228 mpobi123f 36650 mptbi12f 36654 ac6s6 36660 ltrnid 38627 cdleme25dN 38848 nn0rppwr 40848 ntrneiiso 42437 ee323 42864 vd13 42957 vd23 42958 ee03 43097 ee23an 43113 ee32 43115 ee32an 43117 ee123 43119 iccpartgt 45693 stgoldbwt 46042 tgoldbach 46083 nzerooringczr 46444 |
Copyright terms: Public domain | W3C validator |