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 1743 equvel 2455 propeqop 5361 funopsn 6914 xpexr 7642 omordi 8216 omwordi 8221 odi 8229 omass 8230 oen0 8236 oewordi 8241 oewordri 8242 nnmwordi 8285 omabs 8298 fisupg 8833 fiinfg 9029 cantnfle 9200 cantnflem1 9218 pr2ne 9498 gchina 10192 nqereu 10422 supsrlem 10604 1re 10712 lemul1a 11565 xlemul1a 12757 xrsupsslem 12776 xrinfmsslem 12777 xrub 12781 supxrunb1 12788 supxrunb2 12789 difelfzle 13104 addmodlteq 13398 seqcl2 13473 facdiv 13732 facwordi 13734 faclbnd 13735 pfxccat3 14178 dvdsabseq 15751 divgcdcoprm0 16099 2mulprm 16127 exprmfct 16138 prmfac1 16155 pockthg 16335 cply1mul 21062 mdetralt 21352 cmpsub 22144 fbfinnfr 22585 alexsubALTlem2 22792 alexsubALTlem3 22793 ovolicc2lem3 24264 fta1g 24912 fta1 25048 mulcxp 25420 cxpcn3lem 25480 gausslemma2dlem4 26097 colinearalg 26848 upgrwlkdvdelem 27669 umgr2wlk 27879 clwwlknwwlksn 27967 clwwlknonex2lem2 28037 dmdbr5ati 30349 cvmlift3lem4 32847 dfon2lem9 33331 fscgr 34012 colinbtwnle 34050 broutsideof2 34054 a1i14 34119 a1i24 34120 ordcmp 34266 bj-peircestab 34363 wl-aleq 35306 itg2addnc 35443 filbcmb 35510 mpobi123f 35932 mptbi12f 35936 ac6s6 35942 ltrnid 37761 cdleme25dN 37982 nn0rppwr 39894 ntrneiiso 41231 ee323 41650 vd13 41743 vd23 41744 ee03 41883 ee23an 41899 ee32 41901 ee32an 41903 ee123 41905 iccpartgt 44397 stgoldbwt 44746 tgoldbach 44787 nzerooringczr 45148 |
Copyright terms: Public domain | W3C validator |