|   | 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 1735 equvel 2460 propeqop 5511 funopsn 7167 xpexr 7941 resf1extb 7957 omordi 8605 omwordi 8610 odi 8618 omass 8619 oen0 8625 oewordi 8630 oewordri 8631 nnmwordi 8674 omabs 8690 fisupg 9325 fiinfg 9540 cantnfle 9712 cantnflem1 9730 pr2neOLD 10046 gchina 10740 nqereu 10970 supsrlem 11152 1re 11262 lemul1a 12122 xlemul1a 13331 xrsupsslem 13350 xrinfmsslem 13351 xrub 13355 supxrunb1 13362 supxrunb2 13363 difelfzle 13682 addmodlteq 13988 seqcl2 14062 facdiv 14327 facwordi 14329 faclbnd 14330 pfxccat3 14773 dvdsabseq 16351 nn0rppwr 16599 divgcdcoprm0 16703 2mulprm 16731 exprmfct 16742 prmfac1 16758 pockthg 16945 nzerooringczr 21492 cply1mul 22301 mdetralt 22615 cmpsub 23409 fbfinnfr 23850 alexsubALTlem2 24057 alexsubALTlem3 24058 ovolicc2lem3 25555 dvfsumlem2 26068 fta1g 26210 fta1 26351 taylply2 26410 mulcxp 26728 cxpcn3lem 26791 gausslemma2dlem4 27414 colinearalg 28926 upgrwlkdvdelem 29757 umgr2wlk 29970 clwwlknwwlksn 30058 clwwlknonex2lem2 30128 dmdbr5ati 32442 cvmlift3lem4 35328 dfon2lem9 35793 fscgr 36082 colinbtwnle 36120 broutsideof2 36124 a1i14 36302 a1i24 36303 ordcmp 36449 bj-peircestab 36555 wl-aleq 37537 itg2addnc 37682 filbcmb 37748 mpobi123f 38170 mptbi12f 38174 ac6s6 38180 ltrnid 40138 cdleme25dN 40359 ntrneiiso 44109 ee323 44533 vd13 44626 vd23 44627 ee03 44766 ee23an 44782 ee32 44784 ee32an 44786 ee123 44788 iccpartgt 47419 stgoldbwt 47768 tgoldbach 47809 | 
| Copyright terms: Public domain | W3C validator |