![]() |
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 2456 propeqop 5506 funopsn 7141 xpexr 7904 omordi 8562 omwordi 8567 odi 8575 omass 8576 oen0 8582 oewordi 8587 oewordri 8588 nnmwordi 8631 omabs 8646 fisupg 9287 fiinfg 9490 cantnfle 9662 cantnflem1 9680 pr2neOLD 9996 gchina 10690 nqereu 10920 supsrlem 11102 1re 11210 lemul1a 12064 xlemul1a 13263 xrsupsslem 13282 xrinfmsslem 13283 xrub 13287 supxrunb1 13294 supxrunb2 13295 difelfzle 13610 addmodlteq 13907 seqcl2 13982 facdiv 14243 facwordi 14245 faclbnd 14246 pfxccat3 14680 dvdsabseq 16252 divgcdcoprm0 16598 2mulprm 16626 exprmfct 16637 prmfac1 16654 pockthg 16835 cply1mul 21800 mdetralt 22092 cmpsub 22886 fbfinnfr 23327 alexsubALTlem2 23534 alexsubALTlem3 23535 ovolicc2lem3 25018 fta1g 25667 fta1 25803 mulcxp 26175 cxpcn3lem 26235 gausslemma2dlem4 26852 colinearalg 28148 upgrwlkdvdelem 28973 umgr2wlk 29183 clwwlknwwlksn 29271 clwwlknonex2lem2 29341 dmdbr5ati 31653 cvmlift3lem4 34251 dfon2lem9 34701 fscgr 34990 colinbtwnle 35028 broutsideof2 35032 gg-dvfsumlem2 35121 a1i14 35123 a1i24 35124 ordcmp 35270 bj-peircestab 35367 wl-aleq 36342 itg2addnc 36480 filbcmb 36546 mpobi123f 36968 mptbi12f 36972 ac6s6 36978 ltrnid 38944 cdleme25dN 39165 nn0rppwr 41167 ntrneiiso 42775 ee323 43202 vd13 43295 vd23 43296 ee03 43435 ee23an 43451 ee32 43453 ee32an 43455 ee123 43457 iccpartgt 46030 stgoldbwt 46379 tgoldbach 46420 nzerooringczr 46872 |
Copyright terms: Public domain | W3C validator |